\documentstyle[11pt]{article} \addtolength{\textheight}{0.15\textheight} \addtolength{\textwidth}{0.15\textwidth} \setlength{\oddsidemargin}{0.5 in} \setlength{\evensidemargin}{0.5 in} \begin{document} \title{{\bf XMETOO\\User's Manual\\}} \author{The CAMILA Group\\ U. Minho/INESC} \date{November 1990} \maketitle \newpage \tableofcontents \newpage \section{Introduction} \begin{verbatim} xmetoo [Pi89,Ma89] is a functional environment for prototyping formal constructive specifications. It is the kernel prototyping language (often referred to as the basic functional language) of a CASE system for formal software development, still under development at the Computer Science Group of the University of Minho. xmetoo has been designed for prototyping VDM [Jo80,Jo86] specifications: functional definitions can be directly transliterated into xmetoo. On the other hand, to animate relational definitions the user is required to devise a functional (high level) implementation of each operation and test the values returned by applying to them the post-condition, codified as a boolean-valued function. Data type invariants can also be codified as boolean-valued functions. xmetoo is basically an extension to the original Henderson's metoo shell [HM85]. The most relevant extensions are the following: a) Complete implementation of the basic data algebras used in the VDM meta-language as well as a type-checking mechanism. b) Support to user type definition according to the Abstract Syntax rules. All the constructors, selectors and is-functions are automatically defined. c) Implementation of high-order functions (cf. lambda expressions). d) Implementation of an (optional) lazy-evaluator. The interest on laziness is mainly due to the possibility of animation of networks of functional communicating prototypes. e) Implementation of communicating primitives to connect (UNIX) processes running xmetoo interpreters. In particular, they allow the communication of xmetoo structured objects without requiring its previous decomposition. Those primitives can be used to animate specifications of distributed systems. f) Debug facilities. g) Available implementations for UNIX V and MS-DOS. A pre-processor for xmetoo (not described in this Manual) -- called NYAGSL -- is now available [A*89]. It makes possible to write and test the prototypes in a higher level notation, close to that of VDM, and also use a small development shell. The new release of NYAGSL (to be completed in April 1991) will incorporate a LaTex interface so that, from the same NYAGSL source file, both a functional (xmetoo) prototype and a specification document can be generated. NYAGSL is also being enriched with modular facilities. \end{verbatim} \newpage \section{Generics} \begin{verbatim} 2.1 CONFIGURATIONS The basic configuration includes a metoo-like environment with high order functions. Besides, any arrangement of the following configurations is valid: USERTYPE - Supports user defined types. It is the default configuration. LAZY - Includes a lazy-evaluator. COMM - Includes some communication primitives to connect different xmetoo processes under UNIX V. 2.2 PRIMITIVE DATA TYPES a) Symbol - SYM Syntax: any sequence of characters not started with ' ( ) ; " 0..9 -0..-9 +0..+9 \0..\040 and ended by ' ( ) ; " \0..\040 with a maximum of 99 characters. b) String - STR Syntax: any sequence of characters started and ended by ", with a maximum of 100 characters. It may include special characters like: - \e [escape]; - \n [newline]; - \r [return]; - \t [tab]; - \ddd [character whose ascii code is the octal value "ddd'] c) Integer - INT Syntax: not empty sequence of digits, with a signal optional prefix (+ , -) and ended by ' ( ) ; " \0..\040. The subset of Z representable by INT is the one assigned to the int type on the C language (32 bits in UNIX, 16 in MS-DOS) d) Sequences - LIST e) Sets - SET f) Binary Relations - REL g) Finite Functions - FF h) User Defined Functions - FUN i) Shell Functions - SUBR j) File Pointers - FPTR k) Communication Channels - CHAN [Only available in the COMM configuration.] l) TYPE LABEL User Defined Types [Only available in the USERTYPE configuration.] 2.3 EVALUATOR Rules for the evaluation of S-expressions: S-Expression | Type | Value ---------------------------------------------------------------------- nil | () SYM | value linked to the symbol in the current environment STR | the same S-expression INT | the same S-expression SET | the same S-expression REL | the same S-expression FUN | the same S-expression FF | the same S-expression SUBR | the same S-expression FPTR | the same S-expression CHAN | the same S-expression TYPE | error LABEL | error User Defined | error LIST | case 1 - type of (head l) = SUBR : | result of evaluating the shell function applied to (tail l) | case 2 - type of (head l) = FUN : | [LAZY Configuration] result of the evaluation of the | correspondent function applied to (tail l); | [Others Configurations] result of the evaluation of the | correspondent function applied to the evaluation of | each of the elements of (tail l). | case 3 - (head l) = nil | the function identifier, number of arguments and | respective values are shown to the user; the result of the | function is the evaluation of the introduced S-expression. | case 4 - error | Although the type BOOL is not defined, the boolean values "true" and "false" are available. They evaluate for themselves. 2.4 USER INTERACTION * Calling the Interpreter The interpreter is called by the command "xmetoo" at the operating system level (notice it is automatically called when using NYAGSL). Additionally, it is possible to specify a list of text files with xmetoo source code. In that case a "load" statement is executed for each file. * Prompt The interpreter prompt begins each command line. Its general form is: > or n> (being n the number of brackets not yet closed) A command line can have more than one S-expression. * The Trace Stack and Debug The interpreter manages a internal stack storing the expressions whose evaluation is not yet completed. If the evaluation fails, the stack is shown on the screen, starting with the expression in which the error occurred and including all the previous calling levels. The user can also control the step-by-step evaluation of any S-expression by the activation of an internal flag (called the trace-flag) using the primitive function "trace". 2.5 RESERVED WORDS The following symbols cannot be redefined (eg, by the primitives "def" or "deftype"): - "nil" - "true" - "false" - "ops" and "obs" - "oblist" - "stdin" and "stdout" - "empty" - primitive data types identifiers - primitive functions identifiers \end{verbatim} \newpage \section{Notation} \begin{verbatim} 3.1 FUNCTION DEFINITION STRUCTURE The general structure of a primitive function definition is the following: --------------------------------------- N : Function Identifier [Alternative identifiers are presented between brackets.] S : Syntax [Concrete xmetoo syntax.] F : Signature (Functionality) [S-EXP is used as the sort of a polymorphic argument] P : Pre-Condition [Predicate to restrict the primitive function domain. Informal descriptions are presented between square brackets.] D : Description [Informal or semi-formal description of the intended meaning of the primitive function. Informal descriptions are presented between square brackets. The symbol ^= means 'equal by definition'. Unless otherwise stated all the symbols are supposed to be evaluated before use.] --------------------------------------- 3.2 AUXILIAR NOTATION - type( ... ) [returns the type of the argument] - delay( ... ) [returns the current environment needed for the later evaluation of the argument] - let ... in ... [local variables definition] - if ... then ... else ... [conditional] - [sequence enumeration] - {e1, ..., ek} [set enumeration] - [d1->c1, ..., dk->ck] [finite function enumeration] - ... ^ ... [sequence concatenation] - ... div ... [integer division] - ... mod ... [rest of integer division] - ... /\ ... [set intersection] - ... C= ... [subset relation] - el_set( ..., ... ) [set membership relation] - ... andif ... [if not([first argument]) then false else [second argument]] - ... orif ... [if [first argument] then true else [second argument]] - ... != ... [not equal relation] - AL ... . ... [universal quantifier] - EX ... . ... [existential quantifier] - @ ... [returns the value pointed by the argument (cf. S-expression implementation)] Note: Standard BNF notation is freely used throughout this document. \end{verbatim} \newpage \section{Basic Data Models \& Operators} \subsection{Sets} \begin{verbatim} N : card S : (card exp1) F : SET -> INT D : (card e1) ^= [number of elements in set e1 ] --------------------------------- N : choice S : (choice exp1) F : SET -> S-EXP D : exp1 != {} (choice e1) ^= [an element of set e1, chosen non-deterministically) --------------------------------- N : difference S : (difference exp1 exp2) F : SET SET -> SET D : (difference e1 e2) ^= e1 - e2 --------------------------------- N : empty S : empty F : -> SET D : empty ^= {} [denoted by "nil"] --------------------------------- N : intersection S : (intersection exp1 exp2) F : SET SET -> SET D : (intersection e1 e2) ^= e1 /\ e2 --------------------------------- N : isempty S : (isempty exp1) F : SET -> BOOL D : (isempty e1) ^= e1 = {} --------------------------------- N : makeset S : (makeset exp1*) F : S-EXP* -> SET D : (makeset) ^= {} (makeset e1 ... ek) ^= { e1 , ..., ek } --------------------------------- N : member S : (member exp1 exp2) F : S-EXP SET -> BOOL D : (member e1 e2) ^= el_set( e1 , e2 ) --------------------------------- N : reduce S : (reduce exp1 exp2 exp3) F : S-EXP SYM SET -> S-EXP P : [exp2 is an identifier of a binary function] and [the result, the range of the second argument and 'exp1' have the same type] and [all the elements of 'exp3' and 'exp1' have the same type] and ['exp3' != <> ] D : (reduce e s ls) ^= s( x1, s( x2, s( ..., s( xk, e )...))) [where ls = / {x1, ..., xk}] Example: (reduce 0 add (makeset 5 1 6 8 2)) = 22 --------------------------------- N : rel S : (rel exp1 {(from exp2 exp3 [exp4]}+) F : S-EXP {SYM (LIST|SET|REL) [BOOL]}+ -> REL D : (set e1 (from s1 ls1 b1) ... (from sk lsk bk)) ^= [similar to set ...] Example: (rel (pair x y) (from x (makeset 1 3 )) (from y (list 1 2 4 5 2) (not (eq x y)))) = = ((1 2)(1 4)(1 5)(3 1)(3 2)(3 4)(3 5)) --------------------------------- N : set S : (set exp1 {(from exp2 exp3 [exp4]}+) F : S-EXP {SYM (LIST|SET|REL) [BOOL]}+ -> SET D : (set e1 (from s1 ls1 b1) ... (from sk lsk bk)) ^= [The set of elements returned by the evaluation of e1 in the current environment augmented by the symbols s1..sk. The expression 'e1' is evaluated only when each 'si' is bounded to a value from the list/set 'lsi'. Those lists/sets are completely traversed and the predicates 'bi' are tested for each arrangement of values (if omitted a 'bi' is assumed to be true). An arrangement of values is only valid if all 'bi' are verified. The expression 'e1' may be a function on all 'si' as well as on other symbols non local to the "set" expression. The predicates are boolean-valued functions on symbols s1..si-1 and other ones non local to the "set" expression. An 'si' symbol may not be included on the corresponding 'lsi' expression. 'lsi' and 'bi' expressions are partially syntax-checked if any of their sub- expressions define local variables.] Example: (set (mul x y) (from x (makeset 1 3 4)) (from y (list 1 2 4 5 2) (not (eq x y)))) = = (2 4 5 3 6 12 15 8 20) --------------------------------- N : subset S : (subset exp1 exp2) F : SET SET -> BOOL D : (subset e1 e2) ^= e1 C= e2 --------------------------------- N : the S : (the exp1) F : SET -> S-EXP P : [ exp1 is a singleton set] D : (the e1) ^= [the only element of the singleton set e1 ] --------------------------------- N : union S : (union exp1 exp2) F : SET SET -> SET D : (union e1 e2) ^= e1 U e2 --------------------------------- N : UNION S : (UNION exp1) F : SET -> SET P : [ all the members of 'e1' are sets] D : (UNION e1) ^= s1 U s2 U ... U sk [where s1..sk are sets belonging to e1] \end{verbatim} \newpage \subsection{Sequences} \begin{verbatim} N : append S : (append exp1 exp2+) F : LIST LIST+ -> LIST D : (append e1 .. en) ^= e1 ^ .. ^ en --------------------------------- N : CONC S : (CONC exp1) F : LIST -> LIST P : ['exp1' is a list of lists] D : (CONC e1) ^= l1 ^ l2 ^ ... ^ lk [where l1..lk are lists from the list e1 ] --------------------------------- N : cons S : (cons exp1 exp2) F : S-EXP LIST -> LIST D : "non LAZY" Configuration: (cons e1 e2) ^= < e1 > ^ e2 "LAZY" Configuration: (cons e1 e2) ^= ^ delay( e2 ) --------------------------------- N : el ( nth ) S : (el exp1 exp2) F : INT LIST -> S-EXP P : 0 < exp1 <= [lenght of list exp2 ] D : (el e1 e2) ^= [The element of e2 in position e1] --------------------------------- N : elems S : (elems exp1) F : LIST -> SET D : (elems e1) ^= [The set of elements of list e1] --------------------------------- N : head ( hd ) S : (head exp1) F : LIST -> S-EXP P : exp1 != <> D : Non "LAZY" Configurations: (head e1) ^= [first element of e1 ] "LAZY" Configuration: (head e1) ^= if type( e1 ) = "lazy-list" then [first element of e1] else let s1 = e1 in if type( s1 ) = "lazy-list" then [first element of s1] then [first element of s1] --------------------------------- N : inds S : (inds exp1) F : LIST -> LIST D : (inds <>) = <> : (inds e1) ^= [list of natural numbers from 1 to len(s)] --------------------------------- N : length S : (length exp1) F : LIST -> INT D : (length e1) ^= [number of elements of e1 ] --------------------------------- N : list ( makeseq ) S : (list exp1*) F : S-EXP* -> LIST P : (list) ^= <> D :(list e1 ... ek) ^= < e1 ... ek > --------------------------------- N : makeseq ( list ) S : (makeseq exp1*) F : S-EXP* -> LIST P : (makeseq) ^= <> D : (makeseq e1..ek) = < e1 , ..., ek > --------------------------------- N : nil S : nil F : -> LIST D : nil ^= <> --------------------------------- N : pair S : (pair exp1 exp2) F : S-EXP S-EXP -> LIST D : (pair e1 e2) ^= < e1 , e2 > --------------------------------- N : plusq S : (plusq exp1 exp2) F : LIST FF -> LIST P : dom( exp2 ) C= elems( inds( exp1 )) D : (plusq e1 e2) ^= [e1 is overwritten by e2(i) on the positions determined by 'i', belonging to dom( e2 )] Example: let f = ((1 4) (5 3) (2 2)) l = (1 2 3 4 5 6) (plusq l f) = (4 2 3 4 3 6) --------------------------------- N : reduce S : (reduce exp1 exp2 exp3) F : S-EXP SYM LIST -> S-EXP S-EXP SYM SET -> S-EXP P : [exp2 is an identifier of a binary function] and [the result, the range of the second argument and 'exp1' have the same type] and [all the elements of 'exp3' and 'exp1' have the same type] and ['exp3' != <> ] D : (reduce e s ls) ^= s( x1, s( x2, s( ..., s( xk, e )...))) [where ls = / {x1, ..., xk}] Example: (reduce nil cons (list 1 2 1 3 1 4 5 6)) = (1 2 1 3 1 4 5 6) --------------------------------- N : reverse S : (reverse exp1) F : LIST -> LIST D : (reverse e1) ^= [e1 reversed] --------------------------------- N : seq S : (seq exp1 {(from exp2 exp3 [exp4]}+) F : S-EXP {SYM (LIST|SET) [BOOL]}+ -> LIST D : (seq e1 (from s1 ls1 b1) ... (from sk lsk bk)) ^= [The list of elements returned by the evaluation of e1 in the current environment augmented by the symbols s1..sk. The expression 'e1' is evaluated only when each 'si' is bounded to a value from the list/set 'lsi'. Those lists/sets are completely traversed and the predicates 'bi' are tested for each arrangement of values (if omitted a 'bi' is assumed to be true). An arrangement of values is only valid if all 'bi' are verified. The expression 'e1' may be a function on all 'si' as well as on other symbols non local to the "seq" expression. The predicates are boolean-valued functions on symbols s1..si-1 and other ones non local to the "seq" expression. An 'si' symbol may not be included on the corresponding 'lsi' expression. 'lsi' and 'bi' expressions are partially syntax-checked if any of their sub- expressions define local variables.] Example: (seq (list y x) (from x (list 1 2 3 2) (not (eq x 1))) (from y (makeset 'q 'f))) = ((q 2) (f 2) (q 3) (f 3) (q 2) (f 2)) --------------------------------- N : tail ( tl ) S : (tail exp1) F : LIST -> LIST P : exp1 != <> D : Non "LAZY" Configuration: (tail e1) ^= [ e1 without the first element] "LAZY" Configuration: (tail e1) ^= if type( e1 ) = "lazy-list" then [e1 -- not evaluated -- without the first element] else [e1 without the first element] --------------------------------- N : fifth S : (fifth exp1) F : LIST -> S-EXP D : length( exp1 ) >= 5 (fifth e1) ^= [fifth element of e1 ] --------------------------------- N : first S : (first exp1) F : LIST -> S-EXP D : length( exp1 ) >= 1 (first e1) ^= [first element of e1 ] --------------------------------- N : fourth S : (fourth exp1) F : LIST -> S-EXP D : length( exp1 ) >= 4 (fourth e1) ^= [fourth element of e1 ] --------------------------------- N : second S : (second exp1) F : LIST -> S-EXP P : length( exp1 ) >= 2 D : (second e1) ^= [second element of e1 ] --------------------------------- N : third S : (third exp1) F : LIST -> S-EXP D : length( exp1 ) >= 3 (third e1) ^= [third element of e1 ] --------------------------------- \end{verbatim} \newpage \subsection{Finite Functions} \begin{verbatim} N : ap S : (ap exp1 exp2 [exp3]) F : FF S-EXP [S-EXP] -> S-EXP D : (ap e1 e2 e3) ^= let f = e1 s2 = e2 in if el_set( s2, dom( f )) then f(s2) else e3 ["nil" if e3 is omitted] --------------------------------- N : dom S : (dom exp1) F : FF -> SET D : (dom e1) ^= [domain of e1 ] --------------------------------- N : dr S : (dr exp1 exp2) F : FF SET -> FF D : (dr e1 e2) ^= [domain restriction of e1 to e2] Example: (dr ((1 b) (2 g) (8 h) (9 h)) (makeset 1 2)) = ((1 b) (2 g)) --------------------------------- N : ds S : (ds exp1 exp2) F : FF SET -> FF D : (ds e1 e2) ^= [domain subtraction of e2 to e1] Example: (ds ((1 b) (2 g) (8 h) (9 h)) (makeset 1 2)) = ((8 h) (9 h)) --------------------------------- N : ff S : (ff exp1 exp2 exp3 [exp4]) F : SYM SET S-EXP [BOOL] -> FF D : (ff sim set e b) ^= [Finite function whose domain is the set of elements 'sim' from 'set' verifying 'b'. The range is generated by 'e' in the current environment augmented by 'sim'. 'sim' is local to the 'ff' expression, its scope being the expressions 'e' and 'b'. The expressions 'set', 'e' and 'b' are partially syntax-checked if they include subexpressions with local definitions.] Example: (ff x (makeset 1 2 3) (add x 1) (not (eq x 2))) = ((1 2) (3 4)) --------------------------------- N : isempty S : (isempty exp1) F : FF -> BOOL D : (see the section on type SET) --------------------------------- N : makeff S : (makeff {(exp1 exp2)}*) F : {S-EXP S-EXP}* -> FF P : [there are not repeated elements in the domain] D : (makeff) ^= [] (makeff (e1 e2) ... (ek ek+1)) ^= [ e1 -> e2 , ..., ek -> ek+1 ] --------------------------------- N : nil S : nil F : -> FF D : nil ^= [] --------------------------------- N : plus S : (plus exp1 exp2) F : FF FF -> FF D : (plus f1 f2) ^= [Finite function resulting from the overwrite of 'f1' by 'f2'. The domain is the union of the domains of 'f1' and 'f2'. Each element x of the domain is mapped to f1(x), if x is not member of the domain of 'f2', or to f2(x) otherwise.] Example: Let f1 = ((q 2) (w 2) (e 3)) f2 = ((q 3) (r 5) (h 4) (j 2)) in (plus f1 f2) = ((q 3) (w 2) (e 3) (r 5) (h 4) (j 2)) --------------------------------- N : ran S : (ran exp1) F : FF -> SET D : (ran e1) ^= [range of e1 ] --------------------------------- \end{verbatim} \newpage \subsection{Binary Relations} \begin{verbatim} N : card S : (card exp1) F : REL -> INT D : (see the section on type SET) --------------------------------- N : choice S : (choice exp1) F : REL -> S-EXP D : (see the section on type SET) --------------------------------- N : difference S : (difference exp1 exp2) F : REL REL -> REL D : (see the section on type SET) --------------------------------- N : dom S : (dom exp1) F : REL -> SET D : (see the section on type FF) --------------------------------- N : dr S : (dr exp1 exp2) F : REL SET -> REL D : (see the section on type FF) --------------------------------- N : ds S : (ds exp1 exp2) F : REL SET -> REL D : (see the section on type FF) --------------------------------- N : intersection S : (intersection exp1 exp2) F : REL REL -> REL D : (see the section on type SET) --------------------------------- N : isempty S : (isempty exp1) F : REL -> BOOL D : (see the section on type SET) --------------------------------- N : makerel S : (makerel {(exp1 exp2)}*) F : {S-EXP S-EXP}* -> REL D : (makerel) ^= {} (makerel (e1 e2) ... (ek ek+1)) ^= { < e1 , e2 >, ..., < ek , ek+1 >} --------------------------------- N : member S : (member exp1 exp2) F : S-EXP REL -> BOOL D : (see the section on type SET) --------------------------------- N : nil S : nil F : -> REL D : (see the section on type SET) --------------------------------- N : ran S : (ran exp1) F : REL -> SET D : (see the section on type FF) --------------------------------- N : subset S : (subset exp1 exp2) F : REL REL -> BOOL D : (see the section on type SET) --------------------------------- N : the S : (the exp1) F : REL -> S-EXP D : (see the section on type SET) --------------------------------- N : union S : (union exp1 exp2) F : REL REL -> REL D : (see the section on type SET) --------------------------------- \end{verbatim} \newpage \subsection{Integers \& Strings} \begin{verbatim} N : abs S : (abs exp1) F : INT -> INT D : (abs e1) ^= | e1 | --------------------------------- N : add S : (add exp1 exp2) F : INT INT -> INT D : (add e1 e2) ^= e1 + e2 --------------------------------- N : ascii S : (ascii exp1) F : STR -> INT D : (ascii e1) ^= [Ascii code of the first character of 'e1'; 0 is returned if e1="".] --------------------------------- N : atoi S : (atoi exp1) F : STR -> INT D : [numerical string] (atoi e1) ^= [Integer value of the string 'exp1'. Initial spaces are ignored. Only the signal character and the digits until the first no numeric character are considered. Returns 0 in case of error.] --------------------------------- N : chr S : (chr exp1) F : INT -> STR D : (chr e1) ^= [String whose ascii code is 'e1'] --------------------------------- N : div S : (div exp1 exp2) F : INT INT -> INT D : (div e1 e2) ^= e1 div e2 --------------------------------- N : inseg S : (inseg exp1) F : INT -> SET D : (inseg e1) ^= [e1-initial segment of N ( = {1,2,...,e1} )] --------------------------------- N : itoa S : (itoa exp1) F : INT -> STR D : (itoa e1) ^= [String built from the digits and signal of the integer 'e1'] --------------------------------- N : mul S : (mul exp1 exp2) F : INT INT -> INT D : (mul e1 e2) ^= e1 * e2 --------------------------------- N : rem S : (rem exp1 exp2) F : INT INT -> INT D : (rem e1 e2) ^= e1 mod e2 --------------------------------- N : strcat S : (strcat exp1*) F : STR* -> STR P : [The length of the result cannot exceed 100 characters] D : (strcat) ^= "" (strcat e1 ... ek) ^= [Concatenation of the strings 'e1' ... 'ek'] --------------------------------- N : strlen S : (strlen exp1*) F : STR* -> INT D : (strlen) ^= 0 (strlen e1 ... ek) ^= [Sum of the lengths of strings 'e1' to 'ek'] --------------------------------- N : strsym S : (strsym exp1) F : STR -> SYM P : ['exp1' is a string built only from characters used in symbol definition] D : (strsym e1) ^= [symbol built from the sequence of characters in string 'e1'] --------------------------------- N : sub S : (sub exp1 exp2) F : INT INT -> INT D : (sub e1 e2) ^= e1 - e2 --------------------------------- N : substr S : (substr exp1 exp2 [exp3]) F : STR INT [INT] -> STR D : (substr e1 e2 e3) ^= [Substring of 'e1' beginning at position 'e2' and with 'e3' characters. If 'e2' < 1 or if it exceeds the length of 'e1' the result is "" . 'e3' may be omitted; in that case the result will be the tail of 'e1' beginning and including 'e2'. Example: (substr "abcdef" 2) = (substr "abcdef" 2 6) = "bcdef" (substr "abcdef" 2 -1) = "" (substr "abcdef" 2 3) = "bcd" --------------------------------- N : symstr S : (symstr exp1) F : SYM -> STR D : (symstr e1) ^= [String built from the sequence of characters defining 'e1'] --------------------------------- \end{verbatim} \newpage \subsection{Relational Operators} \begin{verbatim} N : eq S : (eq exp1 exp2) F : S-EXP S-EXP -> BOOL D : (eq e1 e2) ^= let s1 = e1 s2 = e2 in (s1 = s2 = nil) orif if (type( s1 ) = type( s2 ) = INT) or (type( s1 ) = type( s2 ) = STR) or (type( s1 ) = type( s2 ) = FPTR) or (type( s1 ) = type( s2 ) = CHAN) or (type( s1 ) = type( s2 ) = SUBR) then @s1 = @s2 else if type( s1 ) = type( s2 ) = SYM then s1 = s2 else false --------------------------------- N : equal S : (equal exp1 exp2) F : S-EXP S-EXP -> BOOL D : (equal e1 e2) ^= (eq e1 e2) orif e1 = e2 --------------------------------- N : geq S : (geq exp1 exp2) F : INT INT -> BOOL STR STR -> BOOL D : (geq e1 e2) ^= e1 >= e2 --------------------------------- N : gt S : (gt exp1 exp2) F : INT INT -> BOOL STR STR -> BOOL D : (gt e1 e2) ^= e1 > e2 --------------------------------- N : leq S : (leq exp1 exp2) F : INT INT -> BOOL STR STR -> BOOL D : (leq e1 e2) ^= e1 <= e2 --------------------------------- N : lt S : (lt exp1 exp2) F : INT INT -> BOOL STR STR -> BOOL D : (lt e1 e2) ^= e1 < e2 --------------------------------- N : neq S : (neq exp1 exp2) F : S-EXP S-EXP -> BOOL D : (neq e1 e2) ^= not( eq( e1 e2 ) ) --------------------------------- N : nequal S : (nequal exp1 exp2) F : S-EXP S-EXP -> BOOL D : (nequal e1 e2) ^= not( equal( e1 e2) ) --------------------------------- \end{verbatim} \newpage \subsection{Logic} \begin{verbatim} N : ALL S : (ALL exp1 exp2 exp3) F : SYM SET BOOL -> BOOL D : (ALL s set pred) ^= [Implementation of the universal quantifier, being 's' the bounded variable, 'set' the quantification domain and 'pred' the predicate. The expressions 'set' and 'pred' are partially syntax-checked if including any local variable definition.] --------------------------------- N : and S : (and exp1 exp2) F : BOOL BOOL -> BOOL D : (and e1 e2) ^= e1 andif e2 --------------------------------- N : EXIST S : (EXIST exp1 exp2 exp3) F : SYM SET BOOL -> BOOL D : (EXIST s set pred) ^= [Implementation of the existential quantifier, being 's' the bounded variable, 'set' the quantification domain and 'pred' the predicate. The expressions 'set' and 'pred' are partially syntax-checked if including any local variable definition.] --------------------------------- N : EXIST1 S : (EXIST1 exp1 exp2 exp3) F : SYM SET BOOL -> BOOL D : (EXIST1 s set pred) ^= [Implementation of the exclusive existential quantifier, being 's' the bounded variable, 'set' the quantification domain and 'pred' the predicate. The expressions 'set' and 'pred' are partially syntax-checked if including any local variable definition.] --------------------------------- N : false S : false F : -> BOOL D : [Boolean constant whose value is false] --------------------------------- N : not S : (not exp1) F : BOOL -> BOOL D : (not e1) ^= if e1 then "true" else "false" --------------------------------- N : or S : (or exp1 exp2) F : BOOL BOOL -> BOOL D : (or e1 e2) ^= e1 orif e2 --------------------------------- N : true S : true F : -> BOOL D : [Boolean constant whose value is true] --------------------------------- \end{verbatim} \newpage \section{Type Definition} \begin{verbatim} N : deftype S : (deftype exp1 exp2) F : SYM -> SYM P : [exp1 cannot be a shell reserved word] D : (deftype t etipo) ^= t [The symbol 't' is linked to the type defined by the expression 'etipo'. No defined type identifiers can appear in 'etipo' and recursive definitions are allowed. The symbol 't' can be used as a constructor of values of the new type. Furthermore, when defining a tuple the labels can be used as selectors (labels with the same name in different tuples are allowed.] NOTE: This is the syntax of type expressions: ::= | | | | | | | ::= | | | | | ::= 'TUP' { '('