Talk:ANSI/ISO C Specification Language

C/C++ Start‑class

	This article is within the scope of WikiProject C/C++, a collaborative effort to improve the coverage of C and C++ topics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.C/C++Wikipedia:WikiProject C/C++Template:WikiProject C/C++C/C++
Start	This article has been rated as Start-class on Wikipedia's content assessment scale.
???	This article has not yet received a rating on the importance scale.

About the syntax section

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.