Re: {Pre,Post}conditions and side effects

[vincent.diemunsch@gmail.com]

Le samedi 25 avril 2015 02:31:57 UTC+2, Bob Duff a écrit :

> Same reason we put comments in the code.  Comments are not "essential
> program logic" in the sense defined above -- if you delete all the
> comments, the program will still work.  But we still want comments.
> Likewise, one should normally write assertions (like Pre and Predicate)
> so the program still works if they are deleted.
> 
> Assertions are like comments, except we have a higher confidence
> that they are actually true.
> 

I agree. Assertions express logical properties of the program. One can have a high
confidence in them for two reasons :
1. mathematical correctness according to a given theory
2. proof that the code is coherent with the assertion, using a tool.

But Assertions should stay as comments, for they are not code but logical formula expressed
in a mathematical langage. They were comments in Spark 05 and it is still the case in Frama-C
or many formal proof systems. Hoare logic is supposed to give "correctness by construction" : 
which is the ability to never fail on a runtime test. This is required in safety critical systems.

But what Ada and SPARK 2014 are doing is "design by contract", as Bertrand Meyer 
called it. This makes a confusion between a precondition and a runtime test. It may
look appealing in the beginning but it is nothing else than a test harness put around
a subprogram. With all the problems related to it : how to debug it ? Should it raise
exceptions ? It breaks the separation between specification and implementation etc.
Therefore, I don't think that it is the right choice for a langage that is mainly used in
safety critical systems.

https://groups.google.com/forum/#!searchin/comp.lang.ada/future$20of$20spark/comp.lang.ada/klr0i37j0uk/5IeGMdlh7PYJ

Kind regards,

Vincent