Code verifications / provers

C code + ACSL annotations --( Frama-C )--> "WhyML" Why3 format Proofs  --( Why3 analyser )--> proven code

• ACSL By Example (good learning point with plenty of exmaples) Towards a Verified C Standard Library

https://www.mimuw.edu.pl/~alx/konstruowanie/ACSL-by-Example.pdf

• Frama-C code analyser (Framework for Modular Analysis of C programs)

https://frama-c.com/
 https://frama-c.com/html/documentation.html 

https://frama-c.com/2016/11/22/Frama-C-and-ACSL-are-on-GitHub.html

• Why3 / WhyML :

http://why3.lri.fr/

http://why3.lri.fr/doc/starting.html

opinion-size-age-shape-colour-origin-material-purpose Noun.

 from a book called The Elements of Eloquence: How to Turn the Perfect English Phrase. 

Adjectives, writes the author, professional stickler Mark Forsyth, “absolutely have to be in this order:

 opinion-size-age-shape-colour-origin-material-purpose Noun. 

So you can have a lovely little old rectangular green French silver whittling knife. But if you mess with that order in the slightest you’ll sound like a maniac.” 

https://getpocket.com/explore/item/how-non-english-speakers-are-taught-this-crazy-english-grammar-rule-you-know-but-have-never-heard-of

Quine : self-replicating program

Quines are programs who print their own source code when run.
For example in lua, this is a quine :

 s="s=%qprint(s:format(s))"print(s:format(s))

• Examples of Quines in Lua


• "The Quine page (self-reproducing code)"


• wikipedia:Quine_(computing)


• Johannes Lötzsch : (Multilanguage) Quines