Re: SPARK code samples

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

Le Wed, 11 Aug 2010 20:00:53 +0200, Ada novice <ycalleecharan@gmx.com> a  
écrit:
> I haven't yet personally written any programs in SPARK but does one
> has necessarily to understand the Z language in order to use SPARK? I
> recall reading somewhere that Barnes's book doesn't discuss the Z
> language (I might be wrong though).

It is not required (just that if I'm not wrong, SPARK itself was checked  
with Z). Z is one the language/method in this area (some are language,  
some others are language and methods), which are mainly : SPARK, Z, B,  
VDM, ACSL (the latter is special, it targets C :p )

You can use SPARK without knowledge of Z, while this may be interesting if  
you can (I just use to know it a few). This is part of culture. Talking  
about culture, in the domain of logic applied to computer science, you may  
be interested into learning about Intuitionistic Logic (deals with  
constructive proof creation, which talks well to computer science)