Talk:ANSI/ISO C Specification Language
 | This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||
| |||||||||||
About the syntax section
[edit]This specification language looks great. If it is a standard, it may not require a lot of references.
Those who can use an specification with pre- and post- conditions, should have a good background in Hoare Logic.
The formal syntax of this specification language should be included. Also a reference table and examples using pre- and post- conditions with the usual HL syntax with the corresponding ACSL translation may help to a better understanding.
Something like this table:
|
Hoare Logic Notation |
ASCL syntax |
Notes |
|---|---|---|
{ HL pre-condition text }
C-statement ;
{ HL post-condition text }
|
/*@ ASCL pre-condition @*/
C-statement ;
/*@ ASCL post-condition @*/
|
comment |
Also an example of the actual output of a simple ACSL annotated program from the corresponding Frama-C will be very helpful.
This is my first table after > 20 years of using wikipedia. I am not sure it that this template can be cut/pasted into the article, it probably needs better formatting parameters. — Preceding unsigned comment added by 201.124.201.209 (talk) 08:36, 22 October 2019 (UTC)
ACSL is not a declarative language is an specification language based in Hoare axiomatic semantics, the last paragraph suggest something that can go in the introduction
[edit]In the description frame says:
Paradigm: Declarative with few imperative features
What does it mean "declarative" when talking about an specification language.
The pre and post-conditions are logical predicates, thus, declarative, which assert what is the state of the actual computation before and after an imperative statement of the language (in this case C) is executed.
The Hoare axioms, triplets formed by
{pre-condition}Statement{post-condition}
are the mean to reason about the behaviour of an imperative program which mutates the state of the variables.
If every pre/post condition is correctly placed, we can be sure, that given an input satisfying the first pre-condition. if the program terminate its execution, it will satisfy the last post-condition. Then we can say that the program is partial correct. In the case that we can also assert that the program always terminate, then it is totally correct.
As you can see, I don't see how ACSL could have a (programming) paradigm attribute, when an specification language like ACSL is used to formally state the semantics of the imperative C language. That is in contrast with the natural language (informal) description in the K&R book or the ISO/ANSI standard.
Moreover, the article could explain that the guys at INRIA an the other institute in France, formally defined the semantics of the ANSI C language, by providing an comments annotation which can be analysed by the Frama-C tool.
They did a great job, because, now, we can know with no ambiguities what a C program does. (Provided that the C compiler that we use complies that specification. Does gcc takes ACSL into account?) — Preceding unsigned comment added by 201.124.201.209 (talk) 09:25, 22 October 2019 (UTC)