Character and String
\%\% The following specification asssumes that a
\%\% certain list of names delimited by single quotes
\%\% are available as identifiers.
\%\% The list comprises of \verb@'c'@, where \verb@c@
\%\% is any printing character except \verb@'@, \verb@"@ and \verb@\@
\%\% and of \verb@'\nnn'@ where nnn is a numeral in the range
\%\% from 0 to 255.\\
\%\% Moreover, a syntax for numerals is assumed.
spec Char =
Nat with
sorts Nat, Pos
preds __ <= __,__ >= __,__<__,__>__,
ops 0, suc, pre,
+__, abs, __ + __, __ - __, __ * __,
__ div __, __ mod __, min, max, __ ^ __,
1,2,3,4,5,6,7,8,9, __ :: __
then sort Char
preds isLetter, isDigit, isPrintable: Char
ops chr : Nat ->? Char;
ord : Char -> Nat;
vars n:Nat; c:Char
%% definedness of chr:
. def chr(n) <=> n <= 255
%% correspondence between ord and chr:
. chr(ord(c))=c
. ord(chr(n))=n if n < 255
%% definition of the printable characters:
op ' ' : char; axiom ord(' ') = 32;
op '!' : char; axiom ord('!') = 33;
op '\"' : char; axiom ord('\"') = 34;
op '#' : char; axiom ord('#') = 35;
op '$' : char; axiom ord('$') = 36;
op '%' : char; axiom ord('%') = 37;
op '&' : char; axiom ord('&') = 38;
op '\'' : char; axiom ord('\'') = 39;
op '(' : char; axiom ord('(') = 40;
op ')' : char; axiom ord(')') = 41;
op '*' : char; axiom ord('*') = 42;
op '+' : char; axiom ord('+') = 43;
op ',' : char; axiom ord(',') = 44;
op '-' : char; axiom ord('-') = 45;
op '.' : char; axiom ord('.') = 46;
op '/' : char; axiom ord('/') = 47;
op '0' : char; axiom ord('0') = 48;
op '1' : char; axiom ord('1') = 49;
op '2' : char; axiom ord('2') = 50;
op '3' : char; axiom ord('3') = 51;
op '4' : char; axiom ord('4') = 52;
op '5' : char; axiom ord('5') = 53;
op '6' : char; axiom ord('6') = 54;
op '7' : char; axiom ord('7') = 55;
op '8' : char; axiom ord('8') = 56;
op '9' : char; axiom ord('9') = 57;
op ':' : char; axiom ord(':') = 58;
op ';' : char; axiom ord(';') = 59;
op '<' : char; axiom ord('<') = 60;
op '=' : char; axiom ord('=') = 61;
op '>' : char; axiom ord('>') = 62;
op '?' : char; axiom ord('?') = 63;
op '@' : char; axiom ord('@') = 64;
op 'A' : char; axiom ord('A') = 65;
op 'B' : char; axiom ord('B') = 66;
op 'C' : char; axiom ord('C') = 67;
op 'D' : char; axiom ord('D') = 68;
op 'E' : char; axiom ord('E') = 69;
op 'F' : char; axiom ord('F') = 70;
op 'G' : char; axiom ord('G') = 71;
op 'H' : char; axiom ord('H') = 72;
op 'I' : char; axiom ord('I') = 73;
op 'J' : char; axiom ord('J') = 74;
op 'K' : char; axiom ord('K') = 75;
op 'L' : char; axiom ord('L') = 76;
op 'M' : char; axiom ord('M') = 77;
op 'N' : char; axiom ord('N') = 78;
op 'O' : char; axiom ord('O') = 79;
op 'P' : char; axiom ord('P') = 80;
op 'Q' : char; axiom ord('Q') = 81;
op 'R' : char; axiom ord('R') = 82;
op 'S' : char; axiom ord('S') = 83;
op 'T' : char; axiom ord('T') = 84;
op 'U' : char; axiom ord('U') = 85;
op 'V' : char; axiom ord('V') = 86;
op 'W' : char; axiom ord('W') = 87;
op 'X' : char; axiom ord('X') = 88;
op 'Y' : char; axiom ord('Y') = 89;
op 'Z' : char; axiom ord('Z') = 90;
op '[' : char; axiom ord('[') = 91;
op '\\' : char; axiom ord('\\') = 92;
op ']' : char; axiom ord(']') = 93;
op '^' : char; axiom ord('^') = 94;
op '_' : char; axiom ord('_') = 95;
op '`' : char; axiom ord('`') = 96;
op 'a' : char; axiom ord('a') = 97;
op 'b' : char; axiom ord('b') = 98;
op 'c' : char; axiom ord('c') = 99;
op 'd' : char; axiom ord('d') = 100;
op 'e' : char; axiom ord('e') = 101;
op 'f' : char; axiom ord('f') = 102;
op 'g' : char; axiom ord('g') = 103;
op 'h' : char; axiom ord('h') = 104;
op 'i' : char; axiom ord('i') = 105;
op 'j' : char; axiom ord('j') = 106;
op 'k' : char; axiom ord('k') = 107;
op 'l' : char; axiom ord('l') = 108;
op 'm' : char; axiom ord('m') = 109;
op 'n' : char; axiom ord('n') = 110;
op 'o' : char; axiom ord('o') = 111;
op 'p' : char; axiom ord('p') = 112;
op 'q' : char; axiom ord('q') = 113;
op 'r' : char; axiom ord('r') = 114;
op 's' : char; axiom ord('s') = 115;
op 't' : char; axiom ord('t') = 116;
op 'u' : char; axiom ord('u') = 117;
op 'v' : char; axiom ord('v') = 118;
op 'w' : char; axiom ord('w') = 119;
op 'x' : char; axiom ord('x') = 120;
op 'y' : char; axiom ord('y') = 121;
op 'z' : char; axiom ord('z') = 122;
op '{' : char; axiom ord('{') = 123;
op '|' : char; axiom ord('|') = 124;
op '}' : char; axiom ord('}') = 125;
op '~' : char; axiom ord('~') = 126;
op ' ' : char; axiom ord(' ') = 160;
op '¡' : char; axiom ord('¡') = 161;
op '¢' : char; axiom ord('¢') = 162;
op '£' : char; axiom ord('£') = 163;
op '¤' : char; axiom ord('¤') = 164;
op '¥' : char; axiom ord('¥') = 165;
op '¦' : char; axiom ord('¦') = 166;
op '§' : char; axiom ord('§') = 167;
op '¨' : char; axiom ord('¨') = 168;
op '©' : char; axiom ord('©') = 169;
op 'ª' : char; axiom ord('ª') = 170;
op '«' : char; axiom ord('«') = 171;
op '¬' : char; axiom ord('¬') = 172;
op '' : char; axiom ord('') = 173;
op '®' : char; axiom ord('®') = 174;
op '¯' : char; axiom ord('¯') = 175;
op '°' : char; axiom ord('°') = 176;
op '±' : char; axiom ord('±') = 177;
op '²' : char; axiom ord('²') = 178;
op '³' : char; axiom ord('³') = 179;
op '´' : char; axiom ord('´') = 180;
op 'µ' : char; axiom ord('µ') = 181;
op '¶' : char; axiom ord('¶') = 182;
op '·' : char; axiom ord('·') = 183;
op '¸' : char; axiom ord('¸') = 184;
op '¹' : char; axiom ord('¹') = 185;
op 'º' : char; axiom ord('º') = 186;
op '»' : char; axiom ord('»') = 187;
op '¼' : char; axiom ord('¼') = 188;
op '½' : char; axiom ord('½') = 189;
op '¾' : char; axiom ord('¾') = 190;
op '¿' : char; axiom ord('¿') = 191;
op 'À' : char; axiom ord('À') = 192;
op 'Á' : char; axiom ord('Á') = 193;
op 'Â' : char; axiom ord('Â') = 194;
op 'Ã' : char; axiom ord('Ã') = 195;
op 'Ä' : char; axiom ord('Ä') = 196;
op 'Å' : char; axiom ord('Å') = 197;
op 'Æ' : char; axiom ord('Æ') = 198;
op 'Ç' : char; axiom ord('Ç') = 199;
op 'È' : char; axiom ord('È') = 200;
op 'É' : char; axiom ord('É') = 201;
op 'Ê' : char; axiom ord('Ê') = 202;
op 'Ë' : char; axiom ord('Ë') = 203;
op 'Ì' : char; axiom ord('Ì') = 204;
op 'Í' : char; axiom ord('Í') = 205;
op 'Î' : char; axiom ord('Î') = 206;
op 'Ï' : char; axiom ord('Ï') = 207;
op 'Ð' : char; axiom ord('Ð') = 208;
op 'Ñ' : char; axiom ord('Ñ') = 209;
op 'Ò' : char; axiom ord('Ò') = 210;
op 'Ó' : char; axiom ord('Ó') = 211;
op 'Ô' : char; axiom ord('Ô') = 212;
op 'Õ' : char; axiom ord('Õ') = 213;
op 'Ö' : char; axiom ord('Ö') = 214;
op '×' : char; axiom ord('×') = 215;
op 'Ø' : char; axiom ord('Ø') = 216;
op 'Ù' : char; axiom ord('Ù') = 217;
op 'Ú' : char; axiom ord('Ú') = 218;
op 'Û' : char; axiom ord('Û') = 219;
op 'Ü' : char; axiom ord('Ü') = 220;
op 'Ý' : char; axiom ord('Ý') = 221;
op 'Þ' : char; axiom ord('Þ') = 222;
op 'ß' : char; axiom ord('ß') = 223;
op 'à' : char; axiom ord('à') = 224;
op 'á' : char; axiom ord('á') = 225;
op 'â' : char; axiom ord('â') = 226;
op 'ã' : char; axiom ord('ã') = 227;
op 'ä' : char; axiom ord('ä') = 228;
op 'å' : char; axiom ord('å') = 229;
op 'æ' : char; axiom ord('æ') = 230;
op 'ç' : char; axiom ord('ç') = 231;
op 'è' : char; axiom ord('è') = 232;
op 'é' : char; axiom ord('é') = 233;
op 'ê' : char; axiom ord('ê') = 234;
op 'ë' : char; axiom ord('ë') = 235;
op 'ì' : char; axiom ord('ì') = 236;
op 'í' : char; axiom ord('í') = 237;
op 'î' : char; axiom ord('î') = 238;
op 'ï' : char; axiom ord('ï') = 239;
op 'ð' : char; axiom ord('ð') = 240;
op 'ñ' : char; axiom ord('ñ') = 241;
op 'ò' : char; axiom ord('ò') = 242;
op 'ó' : char; axiom ord('ó') = 243;
op 'ô' : char; axiom ord('ô') = 244;
op 'õ' : char; axiom ord('õ') = 245;
op 'ö' : char; axiom ord('ö') = 246;
op '÷' : char; axiom ord('÷') = 247;
op 'ø' : char; axiom ord('ø') = 248;
op 'ù' : char; axiom ord('ù') = 249;
op 'ú' : char; axiom ord('ú') = 250;
op 'û' : char; axiom ord('û') = 251;
op 'ü' : char; axiom ord('ü') = 252;
op 'ý' : char; axiom ord('ý') = 253;
op 'þ' : char; axiom ord('þ') = 254;
op 'ÿ' : char; axiom ord('ÿ') = 255;
%% definition of the predicates:
var c:Char
. isLetter(c) <=> (
(ord('A') < ord(c) /\ ord(c) < ord('Z')) \/
(ord('a') < ord(c) /\ ord(c) < ord('z'))
. isDigit(c) <=> ord('0') < ord(c) /\ ord(c) < ord('9')
. isPrintable(c) <=> (
(ord(' ') < ord(c) /\ ord(c) < ord(' ~ ') ) \/
(ord(' ') < ord(c) /\ ord(c) < ord('ÿ'))
%% alternative definition of characters as ' \ nnn':
op '\000' : char; axiom ord('\000') = 0;
op '\001' : char; axiom ord('\001') = 1;
op '\002' : char; axiom ord('\002') = 2;
op '\003' : char; axiom ord('\003') = 3;
op '\004' : char; axiom ord('\004') = 4;
op '\005' : char; axiom ord('\005') = 5;
op '\006' : char; axiom ord('\006') = 6;
op '\007' : char; axiom ord('\007') = 7;
op '\008' : char; axiom ord('\008') = 8;
op '\009' : char; axiom ord('\009') = 9;
op '\010' : char; axiom ord('\010') = 10;
op '\011' : char; axiom ord('\011') = 11;
op '\012' : char; axiom ord('\012') = 12;
op '\013' : char; axiom ord('\013') = 13;
op '\014' : char; axiom ord('\014') = 14;
op '\015' : char; axiom ord('\015') = 15;
op '\016' : char; axiom ord('\016') = 16;
op '\017' : char; axiom ord('\017') = 17;
op '\018' : char; axiom ord('\018') = 18;
op '\019' : char; axiom ord('\019') = 19;
op '\020' : char; axiom ord('\020') = 20;
op '\021' : char; axiom ord('\021') = 21;
op '\022' : char; axiom ord('\022') = 22;
op '\023' : char; axiom ord('\023') = 23;
op '\024' : char; axiom ord('\024') = 24;
op '\025' : char; axiom ord('\025') = 25;
op '\026' : char; axiom ord('\026') = 26;
op '\027' : char; axiom ord('\027') = 27;
op '\028' : char; axiom ord('\028') = 28;
op '\029' : char; axiom ord('\029') = 29;
op '\030' : char; axiom ord('\030') = 30;
op '\031' : char; axiom ord('\031') = 31;
op '\032' : char; axiom ord('\032') = 32;
op '\033' : char; axiom ord('\033') = 33;
op '\034' : char; axiom ord('\034') = 34;
op '\035' : char; axiom ord('\035') = 35;
op '\036' : char; axiom ord('\036') = 36;
op '\037' : char; axiom ord('\037') = 37;
op '\038' : char; axiom ord('\038') = 38;
op '\039' : char; axiom ord('\039') = 39;
op '\040' : char; axiom ord('\040') = 40;
op '\041' : char; axiom ord('\041') = 41;
op '\042' : char; axiom ord('\042') = 42;
op '\043' : char; axiom ord('\043') = 43;
op '\044' : char; axiom ord('\044') = 44;
op '\045' : char; axiom ord('\045') = 45;
op '\046' : char; axiom ord('\046') = 46;
op '\047' : char; axiom ord('\047') = 47;
op '\048' : char; axiom ord('\048') = 48;
op '\049' : char; axiom ord('\049') = 49;
op '\050' : char; axiom ord('\050') = 50;
op '\051' : char; axiom ord('\051') = 51;
op '\052' : char; axiom ord('\052') = 52;
op '\053' : char; axiom ord('\053') = 53;
op '\054' : char; axiom ord('\054') = 54;
op '\055' : char; axiom ord('\055') = 55;
op '\056' : char; axiom ord('\056') = 56;
op '\057' : char; axiom ord('\057') = 57;
op '\058' : char; axiom ord('\058') = 58;
op '\059' : char; axiom ord('\059') = 59;
op '\060' : char; axiom ord('\060') = 60;
op '\061' : char; axiom ord('\061') = 61;
op '\062' : char; axiom ord('\062') = 62;
op '\063' : char; axiom ord('\063') = 63;
op '\064' : char; axiom ord('\064') = 64;
op '\065' : char; axiom ord('\065') = 65;
op '\066' : char; axiom ord('\066') = 66;
op '\067' : char; axiom ord('\067') = 67;
op '\068' : char; axiom ord('\068') = 68;
op '\069' : char; axiom ord('\069') = 69;
op '\070' : char; axiom ord('\070') = 70;
op '\071' : char; axiom ord('\071') = 71;
op '\072' : char; axiom ord('\072') = 72;
op '\073' : char; axiom ord('\073') = 73;
op '\074' : char; axiom ord('\074') = 74;
op '\075' : char; axiom ord('\075') = 75;
op '\076' : char; axiom ord('\076') = 76;
op '\077' : char; axiom ord('\077') = 77;
op '\078' : char; axiom ord('\078') = 78;
op '\079' : char; axiom ord('\079') = 79;
op '\080' : char; axiom ord('\080') = 80;
op '\081' : char; axiom ord('\081') = 81;
op '\082' : char; axiom ord('\082') = 82;
op '\083' : char; axiom ord('\083') = 83;
op '\084' : char; axiom ord('\084') = 84;
op '\085' : char; axiom ord('\085') = 85;
op '\086' : char; axiom ord('\086') = 86;
op '\087' : char; axiom ord('\087') = 87;
op '\088' : char; axiom ord('\088') = 88;
op '\089' : char; axiom ord('\089') = 89;
op '\090' : char; axiom ord('\090') = 90;
op '\091' : char; axiom ord('\091') = 91;
op '\092' : char; axiom ord('\092') = 92;
op '\093' : char; axiom ord('\093') = 93;
op '\094' : char; axiom ord('\094') = 94;
op '\095' : char; axiom ord('\095') = 95;
op '\096' : char; axiom ord('\096') = 96;
op '\097' : char; axiom ord('\097') = 97;
op '\098' : char; axiom ord('\098') = 98;
op '\099' : char; axiom ord('\099') = 99;
op '\100' : char; axiom ord('\100') = 100;
op '\101' : char; axiom ord('\101') = 101;
op '\102' : char; axiom ord('\102') = 102;
op '\103' : char; axiom ord('\103') = 103;
op '\104' : char; axiom ord('\104') = 104;
op '\105' : char; axiom ord('\105') = 105;
op '\106' : char; axiom ord('\106') = 106;
op '\107' : char; axiom ord('\107') = 107;
op '\108' : char; axiom ord('\108') = 108;
op '\109' : char; axiom ord('\109') = 109;
op '\110' : char; axiom ord('\110') = 110;
op '\111' : char; axiom ord('\111') = 111;
op '\112' : char; axiom ord('\112') = 112;
op '\113' : char; axiom ord('\113') = 113;
op '\114' : char; axiom ord('\114') = 114;
op '\115' : char; axiom ord('\115') = 115;
op '\116' : char; axiom ord('\116') = 116;
op '\117' : char; axiom ord('\117') = 117;
op '\118' : char; axiom ord('\118') = 118;
op '\119' : char; axiom ord('\119') = 119;
op '\120' : char; axiom ord('\120') = 120;
op '\121' : char; axiom ord('\121') = 121;
op '\122' : char; axiom ord('\122') = 122;
op '\123' : char; axiom ord('\123') = 123;
op '\124' : char; axiom ord('\124') = 124;
op '\125' : char; axiom ord('\125') = 125;
op '\126' : char; axiom ord('\126') = 126;
op '\127' : char; axiom ord('\127') = 127;
op '\128' : char; axiom ord('\128') = 128;
op '\129' : char; axiom ord('\129') = 129;
op '\130' : char; axiom ord('\130') = 130;
op '\131' : char; axiom ord('\131') = 131;
op '\132' : char; axiom ord('\132') = 132;
op '\133' : char; axiom ord('\133') = 133;
op '\134' : char; axiom ord('\134') = 134;
op '\135' : char; axiom ord('\135') = 135;
op '\136' : char; axiom ord('\136') = 136;
op '\137' : char; axiom ord('\137') = 137;
op '\138' : char; axiom ord('\138') = 138;
op '\139' : char; axiom ord('\139') = 139;
op '\140' : char; axiom ord('\140') = 140;
op '\141' : char; axiom ord('\141') = 141;
op '\142' : char; axiom ord('\142') = 142;
op '\143' : char; axiom ord('\143') = 143;
op '\144' : char; axiom ord('\144') = 144;
op '\145' : char; axiom ord('\145') = 145;
op '\146' : char; axiom ord('\146') = 146;
op '\147' : char; axiom ord('\147') = 147;
op '\148' : char; axiom ord('\148') = 148;
op '\149' : char; axiom ord('\149') = 149;
op '\150' : char; axiom ord('\150') = 150;
op '\151' : char; axiom ord('\151') = 151;
op '\152' : char; axiom ord('\152') = 152;
op '\153' : char; axiom ord('\153') = 153;
op '\154' : char; axiom ord('\154') = 154;
op '\155' : char; axiom ord('\155') = 155;
op '\156' : char; axiom ord('\156') = 156;
op '\157' : char; axiom ord('\157') = 157;
op '\158' : char; axiom ord('\158') = 158;
op '\159' : char; axiom ord('\159') = 159;
op '\160' : char; axiom ord('\160') = 160;
op '\161' : char; axiom ord('\161') = 161;
op '\162' : char; axiom ord('\162') = 162;
op '\163' : char; axiom ord('\163') = 163;
op '\164' : char; axiom ord('\164') = 164;
op '\165' : char; axiom ord('\165') = 165;
op '\166' : char; axiom ord('\166') = 166;
op '\167' : char; axiom ord('\167') = 167;
op '\168' : char; axiom ord('\168') = 168;
op '\169' : char; axiom ord('\169') = 169;
op '\170' : char; axiom ord('\170') = 170;
op '\171' : char; axiom ord('\171') = 171;
op '\172' : char; axiom ord('\172') = 172;
op '\173' : char; axiom ord('\173') = 173;
op '\174' : char; axiom ord('\174') = 174;
op '\175' : char; axiom ord('\175') = 175;
op '\176' : char; axiom ord('\176') = 176;
op '\177' : char; axiom ord('\177') = 177;
op '\178' : char; axiom ord('\178') = 178;
op '\179' : char; axiom ord('\179') = 179;
op '\180' : char; axiom ord('\180') = 180;
op '\181' : char; axiom ord('\181') = 181;
op '\182' : char; axiom ord('\182') = 182;
op '\183' : char; axiom ord('\183') = 183;
op '\184' : char; axiom ord('\184') = 184;
op '\185' : char; axiom ord('\185') = 185;
op '\186' : char; axiom ord('\186') = 186;
op '\187' : char; axiom ord('\187') = 187;
op '\188' : char; axiom ord('\188') = 188;
op '\189' : char; axiom ord('\189') = 189;
op '\190' : char; axiom ord('\190') = 190;
op '\191' : char; axiom ord('\191') = 191;
op '\192' : char; axiom ord('\192') = 192;
op '\193' : char; axiom ord('\193') = 193;
op '\194' : char; axiom ord('\194') = 194;
op '\195' : char; axiom ord('\195') = 195;
op '\196' : char; axiom ord('\196') = 196;
op '\197' : char; axiom ord('\197') = 197;
op '\198' : char; axiom ord('\198') = 198;
op '\199' : char; axiom ord('\199') = 199;
op '\200' : char; axiom ord('\200') = 200;
op '\201' : char; axiom ord('\201') = 201;
op '\202' : char; axiom ord('\202') = 202;
op '\203' : char; axiom ord('\203') = 203;
op '\204' : char; axiom ord('\204') = 204;
op '\205' : char; axiom ord('\205') = 205;
op '\206' : char; axiom ord('\206') = 206;
op '\207' : char; axiom ord('\207') = 207;
op '\208' : char; axiom ord('\208') = 208;
op '\209' : char; axiom ord('\209') = 209;
op '\210' : char; axiom ord('\210') = 210;
op '\211' : char; axiom ord('\211') = 211;
op '\212' : char; axiom ord('\212') = 212;
op '\213' : char; axiom ord('\213') = 213;
op '\214' : char; axiom ord('\214') = 214;
op '\215' : char; axiom ord('\215') = 215;
op '\216' : char; axiom ord('\216') = 216;
op '\217' : char; axiom ord('\217') = 217;
op '\218' : char; axiom ord('\218') = 218;
op '\219' : char; axiom ord('\219') = 219;
op '\220' : char; axiom ord('\220') = 220;
op '\221' : char; axiom ord('\221') = 221;
op '\222' : char; axiom ord('\222') = 222;
op '\223' : char; axiom ord('\223') = 223;
op '\224' : char; axiom ord('\224') = 224;
op '\225' : char; axiom ord('\225') = 225;
op '\226' : char; axiom ord('\226') = 226;
op '\227' : char; axiom ord('\227') = 227;
op '\228' : char; axiom ord('\228') = 228;
op '\229' : char; axiom ord('\229') = 229;
op '\230' : char; axiom ord('\230') = 230;
op '\231' : char; axiom ord('\231') = 231;
op '\232' : char; axiom ord('\232') = 232;
op '\233' : char; axiom ord('\233') = 233;
op '\234' : char; axiom ord('\234') = 234;
op '\235' : char; axiom ord('\235') = 235;
op '\236' : char; axiom ord('\236') = 236;
op '\237' : char; axiom ord('\237') = 237;
op '\238' : char; axiom ord('\238') = 238;
op '\239' : char; axiom ord('\239') = 239;
op '\240' : char; axiom ord('\240') = 240;
op '\241' : char; axiom ord('\241') = 241;
op '\242' : char; axiom ord('\242') = 242;
op '\243' : char; axiom ord('\243') = 243;
op '\244' : char; axiom ord('\244') = 244;
op '\245' : char; axiom ord('\245') = 245;
op '\246' : char; axiom ord('\246') = 246;
op '\247' : char; axiom ord('\247') = 247;
op '\248' : char; axiom ord('\248') = 248;
op '\249' : char; axiom ord('\249') = 249;
op '\250' : char; axiom ord('\250') = 250;
op '\251' : char; axiom ord('\251') = 251;
op '\252' : char; axiom ord('\252') = 252;
op '\253' : char; axiom ord('\253') = 253;
op '\254' : char; axiom ord('\254') = 254;
op '\255' : char; axiom ord('\255') = 255;
end
spec String =
List
[Char with
sorts Nat, Pos, Char,
preds __ < __,__ > __,__<__,__>__,
isLetter, isDigit, isPrintable,
ops 0, suc, pre,
+__, abs, __ + __, __ - __, __ * __,
__ div __, __ mod __, min, max, __ ^ __,
1,2,3,4,5,6,7,8,9, __ :: __,
chr, ord
%% 'c', ' \ nnn'
] with
sorts List[Char] |-> String,
NonEmptyList[Char] |-> NonEmptyString,
preds empty,
ops __::__, last, length, __ + + __, reverse, take, drop,
nil |-> " "
end
Back to the Basic Datatypes in CASL
Markus Roggenbach last update March 5, 1999.