4.2 Some Algebraic Specifications

spec

 DefineOrderedField =

DefineCommutativeField and TotalOrder

then

vars

a,b,c:Elem

.

a+c < b+c if a < b

.

a*c < b*c if a < b /\ c > 0

end

spec

 OrderedField [DefineOrderedField] =

CommutativeField[DefineCommutativeField]

end

spec

 DefineArchimedianField =

DefineOrderedField and Nat

then

sort

Nat < Elem

%%

The embedding is determined by overloading of 0,1,+,<

var

x:Elem

.

exists n:Nat . x<n

end

spec

 ArchimedianField[DefineArchimedianField] =

OrderedField[DefineOrderedField]

end