Re: SPARK

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

Some quick though to feed the talk and give interested parties an  
opportunity to take part.

Although I can understand most of the restrictions SPARK applies (a big  
amount of them did not ever requires to use SPARK to be meaningful and  
beneficial and I do apply lot of them already), I still don't understand  
one : the restriction of not using derived type (except tagged type, which  
are supported by SPARK). What was the rational for that ?

Functions may have legitimate side effects, like for memoisation.  
Memoisation is a kind of optimization and optimizations should be  
transparent to clients. SPARK would requires to split it into two parts: a  
kind of “prepare/compute” procedure and a “get result” function ; the  
procedure being supposedly invoked prior to each function invokation. Did  
you ever face this ?

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 ?

-- 
pragma Asset ? Is that true ? Waaww... great