previous up next
Go up to Example
Go forward to Formulas
RISC-Linz logo

Commands

A Command is one of the following statements executed by the interpreter.

pred Name [ ( ConstrainedVariables ) ] <=> Formula

Defines a predicate with a certain name and arity (number of parameters). Different predicates may have the same name if they have different arities. The symbol `<=>` should be surrounded by whitespace, because it can be also part of a name.

pred isSubset(A: Set, B: Set) <=> // A is subset of B
  forall(x in A: in(x, B)); 
> predicate isSubset/2.
pred positive(x: Nat)<=>>(x, 0);
> ERROR: unexpected '<=>>'.

fun Name [ ( ConstrainedVariables ) ] = Term

Defines a function with a certain name and arity (number of parameters). Different functions may have the same name if they have different arities. The symbol = should be surrounded by whitespace, because it can be also part of a name.

fun **(A: Set, B: Set) =    // the intersection of A and B
  set(x in A: x, in(x, B));
> function **/2.
fun inc(x: Nat)=+(x, 1);
> ERROR: unexpected '=+'.

formula Formula

Evaluates a formula to true or false.

formula isSubset(**(A, B), A);
> true.

term Term

Evaluates a term to a value.

term **(A, **(B, C));
> {1, 2, 3}.

plot Term

Plots a set of points. The value of the given term must be a set of tuples of length 2 that ar interpreted as points in the plane. The elements of each tuple must be natural numbers that are interpreted as the horizontal respectively vertical coordinate of the point. The coordinate system has point (0,0) in the lower left corner and extends swidth units to the right and sheight units to the top. The values swidth and sheight are defined as applet parameters.

plot set(x in nat(1,50), y in nat(1, x): tuple(x, y),
  <=(x,*(y,y)));
> done.

plots Term

Plots a set of point sets. The value of the given term must be a set of point sets as described for the command plot. The point sets are printed in various colors.

plots set(r in nat(1,50):
  set(x in nat(1,r), y in nat(1, x): tuple(x, y),
    <=(x,*(y,y))),
  true);
> done.

read Name

Reads the file Name.txt and executes the commands contained in the file.

read theory/set;
> predicate Subset/2.
> function **/2.
> file 'theory/set.txt' read.

option Option

Sets Option which can be one of the following:

check = ( true | false )

Switches on respectively off the checking of guard formulas and parameter types in the evaluation of formulas and terms.

option check = false;
> guard/parameter checking is off.

universe = Term

Sets the universe of discourse to the domain denoted by the given term. The evaluation of this term must denote a domain (a set). All quantified variables without domain constraints are assumed to range over this domain.

option universe = nat(1,100);
> universe of discourse set.

help

Prints a short help message with a reference to this Web page.

help;
> commands (terminated by ';'):
>   pred <name>(<parameters>) <=> <formula>;
>   fun <name>(<parameters>) = <term>;
>   formula <formula>;
>   term <term>;
>   plot <term>;
>   plots <term>;
>   read <name>;
>   option <name> = <value>;
>   help;
> see http://www.risc.uni-linz.ac.at/software/formal.

Maintained by: Wolfgang Schreiner
Last Modification: July 6, 1999

previous up next