Footnotes

 

(1)

The annotations lead to proof obligations, which can be later discharged with a theorem proving tool, increasing the trust in the correctness of the specifications.  

(2)

%[div_Nat_total] is a special case of %[div_Nat_partial]; %[div_Nat_partial] implies forall s:Nat. ¬ (m div 0) = s , therefore ¬ def ( m div 0 ) .  

(3)

To be precise, we also have to remove the subsorts from the generation of natural numbers in GenerateNat.  

(4)

The only exception is the specification Group, which is syntactically correct but can by the Bremen parser not be parsed as the static analysis of structured specifications is not yet fully supported.  

(5)

We have rewritten the annotations as comments. Further we had to fix errors caused by the translation with hyperlatex: sometimes the space character disappears, sometimes a space character appears and makes two operator names from one operator name, the comment signs %% appear in another line than the comment etc.  

(6)

in subsection 3.7 "Finite Sets"  

(7)

in subsection 3.6 "Numbers"  

(8)

in subsection 3.6 "Numbers"  

(9)

in subsection 3.7 "Finite Sets"  

(10)

in subsection 3.10 "Exact Fixed Point Numbers"  

(11)

Please note the version of the study note [RM99]. There is an ongoing discussion concerning annotations with definite decisions only for some annotations. Thus for this version of the "Basic Datatypes in CASL" we use our first proposal of annotations, which is documented in a study note.