Prev Up Next
Go backward to 2.4 Library Numbers
Go up to 2 Specifications
Go forward to 2.6 Library StructuredDatatypes

2.5 Library SimpleDatatypes

library Basic/SimpleDatatypes 
version 0.3
%% authors: M.Roggenbach, T.Mossakowski
%% date: 1.11.99

from Basic/Orders version 0.3 get BooleanAlgebra
from Basic/Numbers version 0.3 get Nat

spec
Boolean =
free type
Boolean ::= TRUE | FALSE
%%
intended system of representatives:
%%
TRUE, FALSE
ops
NOT__ : Boolean -> Boolean;
__AND__, __OR__ : Boolean ×Boolean -> Boolean
%prec
__OR__ < __AND__
vars
x,y,z:Boolean
.
%[NOT_FALSE] NOT(FALSE)=TRUE
.
%[NOT_TRUE] NOT(TRUE)=FALSE
.
%[AND_def1] FALSE AND FALSE = FALSE
.
%[AND_def2] FALSE AND TRUE = FALSE
.
%[AND_def3] TRUE  AND FALSE = FALSE
.
%[AND_def4] TRUE  AND TRUE = TRUE
.
%[OR_def] x OR y=NOT(NOT(x) AND NOT(y))
end
view
BooleanAlgebra_in_Boolean:
DefineBooleanAlgebra to Boolean
=
sort
Elem |-> Boolean,
ops
0 |-> FALSE,
1 |-> TRUE,
__ |¯| __ |-> __AND__,
__ |_| __ |-> __OR__
end

Here we only give part of the specification Char to present its structure. The complete specification can be found in

http://www.informatik.uni-bremen.de/~cofi/CASL/lib/basic/
We assume that a certain list of names delimited by single quotes is available as identifiers. The list comprises of 'c', where c is any printing character except one of the three characters ', " and \. These characters are represented as '\' ', '\" ', and '\\', resp. Furthermore this list consists of elements ' \ nnn', where nnn is a numeral in the range from 0 to 255. Moreover, a syntax for numerals is assumed.
spec
Char =
Nat
then
sort
Char
preds
isLetter, isDigit, isPrintable: Char
ops
chr : Nat ->? Char;
ord : Char -> Nat;
vars
n:Nat; c:Char
.
%[chr_dom] def chr(n) <=> n <= 255
.
%[chr_def] chr(ord(c))=c
.
%[ord_def] ord(chr(n))=n if n < 255
%%
definition of the printable characters:
op
' ' : Char; axiom %[ord_32] ord(' ') = 32;
op
'!' : Char; axiom %[ord_33] ord('!') = 33;
op
'\" ': Char; axiom %[ord_34] ord('\"') = 34;
op
'#': Char; axiom %[ord_35] ord('#') = 35;
...
op
'&' : Char; axiom %[ord_38] ord('&') = 38;
op
'\' ': Char; axiom %[ord_39] ord('\' ') = 39;
op
'(': Char; axiom %[ord_40] ord('(') = 40;
...
op
'0' : Char; axiom %[ord_48] ord('0') = 48;
...
op
'9' : Char; axiom %[ord_57] ord('9') = 57;
...
op
'A' : Char; axiom %[ord_65] ord('A') = 65;
...
op
'Z' : Char; axiom %[ord_90] ord('Z') = 90;
...
op
'{': Char; axiom %[ord_91] ord('{') = 91;
op
'\\': Char; axiom %[ord_92] ord('\\') = 92;
op
'}': Char; axiom %[ord_93] ord('}') = 93;
...
op
'a' : Char; axiom %[ord_97] ord('a') = 97;
...
op
'z' : Char; axiom %[ord_122] ord('z') = 122;
op
'{' : Char; axiom %[ord_123] ord('{') = 123;
...
...
op
' ~ ' : Char; axiom %[ord_126] ord(' ~ ') = 126;
%%
and all Characters c with 161 < ord(c) < 255:
op
' ' : Char; axiom %[ord_160] ord(' ') = 160;
...
op
'ÿ' : Char; axiom %[ord_255] ord('ÿ') = 255;
%%
definition of the predicates:
.
%[isLetter_def]
isLetter(c) <=> (
(ord('A') < ord(c) /\ ord(c) < ord('Z')) \/
(ord('a') < ord(c) /\ ord(c) < ord('z')) )
.
%[isDigit_def]
isDigit(c) <=> ord('0') < ord(c) /\ ord(c) < ord('9')
.
%[isPrintable_def]
isPrintable(c) <=> (
(ord(' ') < ord(c) /\ ord(c) < ord(' ~ ') ) \/
(160 < ord(c) /\ ord(c) < ord('ÿ')) )
%%
alternative definition of characters as ' \ nnn':
op
' \ 000' : Char; axiom %[slash_000] ord(' \ 000') = 0;
op
' \ 001' : Char; axiom %[slash_001] ord(' \ 001') = 1;
...
op
' \ 254' : Char; axiom %[slash_254] ord(' \ 254') = 254;
op
' \ 255' : Char; axiom %[slash_255] ord(' \ 255') = 255;
end
CoFI Note: L-12 -- Version: 0.3 -- November 1999.
Comments to cofi@informatik.uni-bremen.de

Prev Up Next