from Basic/Numbers get Int

spec PredefinedSign =

Int with Int |-> integer, Nat |-> nonNegativeInteger, Pos |-> positiveInteger

then

sort Thing

sort boolean < DATA

sort integer < DATA

op True,False:boolean

sort positveInteger < nonNegativeInteger;

sort nonNegativeInteger < integer;

sort nonPositiveInteger < integer;

sort negativeInteger < nonPositiveInteger;

sort nonPositiveInteger = {p : integer . p <= 0}

pred Nothing : Thing

forall x : nonNegativeInteger

. 0 @@ x = x %(no_preceeding_zeros)%

forall x : Thing . not (Nothing (x)) %(gn_Nothing_def)%

sorts Char; string < DATA

free type string ::= emptyString | __:@:__ (Char;string)

ops ' ' : Char; %(DL_printable_32)%

'!' : Char; %(DL_printable_33)%

'\"' : Char; %(DL_printable_34)%

'#' : Char; %(DL_printable_35)%

'$' : Char; %(DL_printable_36)%

'%' : Char; %(DL_printable_37)%

'&' : Char; %(DL_printable_38)%

'\'' : Char; %(DL_printable_39)%

'(' : Char; %(DL_printable_40)%

')' : Char; %(DL_printable_41)%

'*' : Char; %(DL_printable_42)%

'+' : Char; %(DL_printable_43)%

',' : Char; %(DL_printable_44)%

'-' : Char; %(DL_printable_45)%

'.' : Char; %(DL_printable_46)%

'/' : Char; %(DL_printable_47)%

'0' : Char; %(DL_printable_48)%

'1' : Char; %(DL_printable_49)%

'2' : Char; %(DL_printable_50)%

'3' : Char; %(DL_printable_51)%

'4' : Char; %(DL_printable_52)%

'5' : Char; %(DL_printable_53)%

'6' : Char; %(DL_printable_54)%

'7' : Char; %(DL_printable_55)%

'8' : Char; %(DL_printable_56)%

'9' : Char; %(DL_printable_57)%

':' : Char; %(DL_printable_58)%

';' : Char; %(DL_printable_59)%

'<' : Char; %(DL_printable_60)%

'=' : Char; %(DL_printable_61)%

'>' : Char; %(DL_printable_62)%

'?' : Char; %(DL_printable_63)%

'@' : Char; %(DL_printable_64)%

'A' : Char; %(DL_printable_65)%

'B' : Char; %(DL_printable_66)%

'C' : Char; %(DL_printable_67)%

'D' : Char; %(DL_printable_68)%

'E' : Char; %(DL_printable_69)%

'F' : Char; %(DL_printable_70)%

'G' : Char; %(DL_printable_71)%

'H' : Char; %(DL_printable_72)%

'I' : Char; %(DL_printable_73)%

'J' : Char; %(DL_printable_74)%

'K' : Char; %(DL_printable_75)%

'L' : Char; %(DL_printable_76)%

'M' : Char; %(DL_printable_77)%

'N' : Char; %(DL_printable_78)%

'O' : Char; %(DL_printable_79)%

'P' : Char; %(DL_printable_80)%

'Q' : Char; %(DL_printable_81)%

'R' : Char; %(DL_printable_82)%

'S' : Char; %(DL_printable_83)%

'T' : Char; %(DL_printable_84)%

'U' : Char; %(DL_printable_85)%

'V' : Char; %(DL_printable_86)%

'W' : Char; %(DL_printable_87)%

'X' : Char; %(DL_printable_88)%

'Y' : Char; %(DL_printable_89)%

'Z' : Char; %(DL_printable_90)%

'[' : Char; %(DL_printable_91)%

'\\' : Char; %(DL_printable_92)%

']' : Char; %(DL_printable_93)%

'^' : Char; %(DL_printable_94)%

'_' : Char; %(DL_printable_95)%

'`' : Char; %(DL_printable_96)%

'a' : Char; %(DL_printable_97)%

'b' : Char; %(DL_printable_98)%

'c' : Char; %(DL_printable_99)%

'd' : Char; %(DL_printable_100)%

'e' : Char; %(DL_printable_101)%

'f' : Char; %(DL_printable_102)%

'g' : Char; %(DL_printable_103)%

'h' : Char; %(DL_printable_104)%

'i' : Char; %(DL_printable_105)%

'j' : Char; %(DL_printable_106)%

'k' : Char; %(DL_printable_107)%

'l' : Char; %(DL_printable_108)%

'm' : Char; %(DL_printable_109)%

'n' : Char; %(DL_printable_110)%

'o' : Char; %(DL_printable_111)%

'p' : Char; %(DL_printable_112)%

'q' : Char; %(DL_printable_113)%

'r' : Char; %(DL_printable_114)%

's' : Char; %(DL_printable_115)%

't' : Char; %(DL_printable_116)%

'u' : Char; %(DL_printable_117)%

'v' : Char; %(DL_printable_118)%

'w' : Char; %(DL_printable_119)%

'x' : Char; %(DL_printable_120)%

'y' : Char; %(DL_printable_121)%

'z' : Char; %(DL_printable_122)%

'{' : Char; %(DL_printable_123)%

'|' : Char; %(DL_printable_124)%

'}' : Char; %(DL_printable_125)%

'~' : Char; %(DL_printable_126)%

%% Iso-Latin-1 character number 160 is displayed as space,

%% but internally is different from character 32 (space)

'�' : Char; %(DL_printable_160)%

'�' : Char; %(DL_printable_161)%

'�' : Char; %(DL_printable_162)%

'�' : Char; %(DL_printable_163)%

'�' : Char; %(DL_printable_164)%

'�' : Char; %(DL_printable_165)%

'�' : Char; %(DL_printable_166)%

'�' : Char; %(DL_printable_167)%

'�' : Char; %(DL_printable_168)%

'�' : Char; %(DL_printable_169)%

'�' : Char; %(DL_printable_170)%

'�' : Char; %(DL_printable_171)%

'�' : Char; %(DL_printable_172)%

'�' : Char; %(DL_printable_173)%

'�' : Char; %(DL_printable_174)%

'�' : Char; %(DL_printable_175)%

'�' : Char; %(DL_printable_176)%

'�' : Char; %(DL_printable_177)%

'�' : Char; %(DL_printable_178)%

'�' : Char; %(DL_printable_179)%

'�' : Char; %(DL_printable_180)%

'�' : Char; %(DL_printable_181)%

'�' : Char; %(DL_printable_182)%

'�' : Char; %(DL_printable_183)%

'�' : Char; %(DL_printable_184)%

'�' : Char; %(DL_printable_185)%

'�' : Char; %(DL_printable_186)%

'�' : Char; %(DL_printable_187)%

'�' : Char; %(DL_printable_188)%

'�' : Char; %(DL_printable_189)%

'�' : Char; %(DL_printable_190)%

'�' : Char; %(DL_printable_191)%

'�' : Char; %(DL_printable_192)%

'�' : Char; %(DL_printable_193)%

'�' : Char; %(DL_printable_194)%

'�' : Char; %(DL_printable_195)%

'�' : Char; %(DL_printable_196)%

'�' : Char; %(DL_printable_197)%

'�' : Char; %(DL_printable_198)%

'�' : Char; %(DL_printable_199)%

'�' : Char; %(DL_printable_200)%

'�' : Char; %(DL_printable_201)%

'�' : Char; %(DL_printable_202)%

'�' : Char; %(DL_printable_203)%

'�' : Char; %(DL_printable_204)%

'�' : Char; %(DL_printable_205)%

'�' : Char; %(DL_printable_206)%

'�' : Char; %(DL_printable_207)%

'�' : Char; %(DL_printable_208)%

'�' : Char; %(DL_printable_209)%

'�' : Char; %(DL_printable_210)%

'�' : Char; %(DL_printable_211)%

'�' : Char; %(DL_printable_212)%

'�' : Char; %(DL_printable_213)%

'�' : Char; %(DL_printable_214)%

'�' : Char; %(DL_printable_215)%

'�' : Char; %(DL_printable_216)%

'�' : Char; %(DL_printable_217)%

'�' : Char; %(DL_printable_218)%

'�' : Char; %(DL_printable_219)%

'�' : Char; %(DL_printable_220)%

'�' : Char; %(DL_printable_221)%

'�' : Char; %(DL_printable_222)%

'�' : Char; %(DL_printable_223)%

'�' : Char; %(DL_printable_224)%

'�' : Char; %(DL_printable_225)%

'�' : Char; %(DL_printable_226)%

'�' : Char; %(DL_printable_227)%

'�' : Char; %(DL_printable_228)%

'�' : Char; %(DL_printable_229)%

'�' : Char; %(DL_printable_230)%

'�' : Char; %(DL_printable_231)%

'�' : Char; %(DL_printable_232)%

'�' : Char; %(DL_printable_233)%

'�' : Char; %(DL_printable_234)%

'�' : Char; %(DL_printable_235)%

'�' : Char; %(DL_printable_236)%

'�' : Char; %(DL_printable_237)%

'�' : Char; %(DL_printable_238)%

'�' : Char; %(DL_printable_239)%

'�' : Char; %(DL_printable_240)%

'�' : Char; %(DL_printable_241)%

'�' : Char; %(DL_printable_242)%

'�' : Char; %(DL_printable_243)%

'�' : Char; %(DL_printable_244)%

'�' : Char; %(DL_printable_245)%

'�' : Char; %(DL_printable_246)%

'�' : Char; %(DL_printable_247)%

'�' : Char; %(DL_printable_248)%

'�' : Char; %(DL_printable_249)%

'�' : Char; %(DL_printable_250)%

'�' : Char; %(DL_printable_251)%

'�' : Char; %(DL_printable_252)%

'�' : Char; %(DL_printable_253)%

'�' : Char; %(DL_printable_254)%

'�' : Char; %(DL_printable_255)%

end