Re: SPARK

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Thu, 13 May 2010 05:06:23 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> Block statements are not allowed in SPARK. Let say a procedure can do  
> the same. Was this only to have one-matter-one-feature (avoid to have  
> both block-statement and procedure, and keep only one) for the sake of  
> simplicity or was there some other reasons properly dealing with  
> verifiability ?

Here is an answer:

A document from SparkSure ( http://www.sparksure.com/7.html ), namely  
Part4_Multiple_Paths.pdf, warns about consecutive conditional statements,  
giving the example of ten simple chained If statement which turns into  
1024 validation conditions. In this document, Phil logically advice to  
avoid such cases, using small procedures instead. Doing so, you end up  
with a single path instead of 1014.

So far this is not about blocks, however here comes the matter: block  
statements does not break such a chain of If statements and cannot be  
given annotations. Lack of annotations with block statement makes these  
ineffective to reach the goal of simplifying the program provability.

So why not annotations on block statements ? Well, simply because a block  
statement does not come with a signature and using a procedure instead of  
a block statement, requires you to better specify what was the role of  
that block. And adding extra-annotations to the language, to be used with  
blocks, would just load the language with unnecessary complications (not  
welcome in this area)

Finally, block statements are disallowed to help avoid explosive  
complexity.

-- 
There is even better than a pragma Assert: an --# assert