[Index] || [Contents]

Disclaimer. CSUSB and the CS Dept have no responsibility for it.

This is a Beta Version, read at your own risk.

Copyright. Richard J. Botting(Sun Jul 6 10:03:41 PDT 2003). This paper is being developed for publication. Permission is granted to quote parts of it as long as the source is acknowledged and the author informed.

- Relational Semantics of The While Language
- : Main Text
- : : Motto
- : : Introduction
- : : Relations
- : : Syntax and Semantics
- : : : Method
- : : : Abstract Syntax of While
- : : : Example of a Program
- : : : Terminology
- : : : Semantic Domains
- : : : : Numbers
- : : : : Variables
- : : : : Example of a State Space
- : : : : Expressions
- : : : : Change of State
- : : : Semantic Equations
- : : : : Semantic Equations for Num
- : : : : Exercises on the Semantics of Num
- : : : : Semantics of Var
- : : : : Example of Semantics of Var
- : : : : Semantics of Aexp
- : : : : Example of Semantics of Aexp
- : : : : Exercises on Semantics of Aexp
- : : : : Semantics of Bexp
- : : : : Example of Semantics of Bexp
- : : : : Exercises on Semantics of Bexp
- : : : : Relational Semantics of Stm
- : : : : Example of Semantics of a Program
- : : : : Exercises on the Relational Semantics of Aexp
- : : Conclusion
- : Footnotes
- : : XBNF
- : : Calculus of Relations
- : : State Space
- : : Dynamic Predicates
- : : : Conditions as Static Predicates
- : : : Assignments
- : : : General Form
- : : CoProducts
- : : Structural Operational Semantics
- : : : Exercise on Structural Operational Semantics
- Index of defined terms etc.

- (kleene): {}, Id, Id|R, Id|R|R;R, Id|R|R;R|R;R;R, ...
- generated by
- (generator): S'=Id | S;R
- has a least upper bound or limit of
- (limit): do(R).
The above formulae use notations for the identity relation(Id), the
union(|) and composition(;) of relations, and the reflexive and transitive
closure(do) of relations: See
[ Calculus of Relations ]
### Syntax and Semantics

#### Method

I use a generalized version of BNF to define Syntax and Semantics called XBNF. The syntax is defined in a form close to traditional EBNF. The semantics is defined by a grammar of functions and relations. The details are below: [ XBNF ]I use the symbol

*m*to indicate denotations:*m(C)*indicates the "meaning of C". The symbol*m*indicates the function that maps*C*into*m(C)*. For each syntactic category*Syn*, there is a set of meanings - a semantic domain*Sem*say, and*m*maps each element of*Syn*into and element of*Sem*: - m::Syn->Sem.
The semantic domain is determined by the Syntax of the argument to which

*m*is applied: For example*m("101")*gives a number but*m("while 1<x do x:=x-1")*is a relationship between describing what can possibly happen. See [ CoProducts ] for the justification of this idea.Two items

*C1*,*C2*in the same syntactic category are*equivalent*if and only if*m(C1) = m(C2)*. Items in different syntactic categories can not be equivalent.#### Abstract Syntax of While

- grammar_of_While::= Net{
- Num::syntax=
*Numbers, here binary is used, but could be in decimal.*. - Var::syntax=
*A set of variables, here letters are used*. - Aexp::syntax=
*The arithmetic expressions giving numbers as values*. - Bexp::syntax=
*Boolean expressions, giving tt or ff as values* - Stm::syntax=
*Statements*. - Num::= "0" | "1" | Num "0" | Num "1".
- Aexp::= Num | Var | Aexp "*" Aexp | Aexp "+" Aexp | Aexp "-" Aexp.
- Bexp::= "true" | "false" | Aexp "=" Aexp | Aexp "<=" Aexp | "~" Bexp | Bexp "/\" Bexp.
- Stm::= Var ":=" Aexp | "skip" | Stm";" Stm | "if" Bexp "then" Stm
"else" Stm | "while" Bexp "do" S.

After Neilsen & Neilsen 92.

}=::grammar_of_While.#### Example of a Program

Suppose Var={"x", "y" , "z" } and F:="(z:=1; y:=x); while ( 1 <= y ) do ( z:=z*y; y:=y-1 ))", then F \in Stm.

#### Terminology

The following words are used for talking about the While language: - Num::syntax=
- assignment::= Var:=Aexp.
- sequence::= Stm; Stm.
- selection::= if Bexp then Stm else Stm.
- loop::=iteration,
- iteration::=while Bexp do S.
#### Semantic Domains

In the following I assume that we have the whole of abstract algebra available to us when we wish to define how a program behaves. The alternative is to spend time re-inventing wheels. The necessary algebras are listed in this section. They are used in the following section: [ Semantic Equations ]##### Numbers

I assume that a number is in a ring with addition, subtraction, multiplication, zero, and unit - with the usual rules and assumptions: - number::ring((+),(-),0,(*), (1) ),
[ Rings in math_41_Two_Operators ]
We normally assume some extra rules: Here I need there to exist a distinct number

- 2::number=1+1.
This is so that I can formally define the meaning of a binary (base 2)

*Num*as a distinct element of the ring*number*.Normally the numbers are taken to be the integers, however see Hoare 69, C.A.R. Hoare, An Axiomatic Basis for Computer Programming, Commun ACM V12 n10 Oct 69.

##### Variables

In the*While*language without declarations, each identifier always identifies the same variable. I introduce a function that associates each symbol in*Var*with a corresponding name of a field in record structure (or labeled tuple). The set of all possible records is called the State: - State::=${ x,y,z, ... :number. }.
Here ${...v:S...} is a notation for the mathematical objects normally
implemented as records or structures.
Each of
*x*,*y*,*z*, etc are functions in*State->number*. For details see [ State Space ]This is not the traditional approaches where a state is a function mapping elements of

*Var*into current values, or where a state associates*Var*s with locations and locations with current values..##### Example of a State Space

Suppose Var={"x", "y" , "z" } then State = ${ x,y,z::number }, and a typical state would be*State(x=>1, y=>2, z=>3)*. The function*m:Var->{x,y,z}*then maps "x" into*x*, "y" into*y*, and "z" into*y*: - m= ("x"+>x | "y"+>y | "z"+> z)
- = {("x", x) , ("y", y), ( "z", z) }.
##### Expressions

The semantic domain for*Aexp*is typically those of numbers -*values*in the target algebra. However because I start from assuming that we have an abstract algebra (not just an abstract data type) we can associate each*Aexp*in*While*to an expression in the algebra of*number*-- in the set*expression(number)*. We can now use these expressions in predicates and get simpler rules defining the behavior of assignments.##### Change of State

The heart of relational semantics is the natural model for change: a relation between two states, before and after: - Change::=@(State,State). I distinguish (in case they are useful), two special sets of Change:
- Condition::@Change={ R:Change | for all x,y:State, x R y implies x = y }.
- Action::@Change={ R:Change | for all x:State, one y :State, x R y }.
A relation R:Change is [ determinstic ] when for each

*s*there is no more than one*s'*such that*s R s'*. A relation is [ total ] when for each*s*there is at least one*s'*. Functions are both total and deterministic. Partial functions are deterministic but not total. One to one relations are determinsistic, and so are there inverse or converse.Exercise: Show that all conditions are deterministic. Show that all Actions are deterministic.

Exercise: Are all Actions functions? Are any Conditions functions?

*. . . . . . . . . ( end of section Semantic Domains)*<<Contents | Index>>#### Semantic Equations

##### Semantic Equations for Num

These are a simple introduction to the method, not a useful notation.For n:Num, m(

*n*)::number. - m("0")::= 0,
- m("1")::= 1,
For n:Num, d:{"0", "1"}, m(n d) ::=2 * m(n) + m(d).
##### Exercises on the Semantics of Num

Exercise: Is*m*on Num a total function or a partial function? Is it a one-to-one function or many-to-one function? If many to one derive a congruence so that strings modulo the congruence are semantically equivalent.##### Semantics of Var

- m::Var->expression(number).
In fact I assume that for each item in Var (say "x") there is a
corresponding component in a state record that is used to express numbers.
See below:
[ State Space ]
for a more typical model of such a state space.
##### Example of Semantics of Var

Suppose Var={"x", "y" , "z" } then State = ${ x,y,z::number }, and a typical state would be*s=State(x=>1, y=>2, z=>3)*. The function*m:Var->{x,y,z}*then maps "x" into*x*, "y" into*y*, and "z" into*y*: - m= ("x"+>x | "y"+>y | "z"+> z)
- = {("x", x) , ("y", y), ( "z", z) }.
Hence, m("x") =x and s.m("x")=1 and s.m("y")=2 and s.m("z")=3.
##### Semantics of Aexp

- m::Aexp->expression(number). Notice that Var and Num are subsets of Aexp so that their meaning is already defined above.
- For a1,a2:Aexp, m(a1 "+" a2)::= m(a1) + m(a2),
- For a1,a2:Aexp, m(a1 "*" a2)::= m(a1) * m(a2),
- For a1,a2:Aexp, m(a1 "-" a2)::= m(a1) - m(a2).
##### Example of Semantics of Aexp

Suppose Var={"x", "y" , "z" } then State = ${ x,y,z::number }, and a typical state would be*s=State(x=>1, y=>2, z=>3)*. The function*m:Var->{x,y,z}*then maps "x" into*x*, "y" into*y*, and "z" into*y*: - m= ("x"+>x | "y"+>y | "z"+> z)
- = {("x", x) , ("y", y), ( "z", z) }.
Hence, m("x") =x and s.m("x")=1 and s.m("y")=2 and s.m("z")=3.

- :. m("x+y") = m("x") + m("y") = x+y.
However, m("x+y") is not 3 but

*x+y*. In state*s*=(x=>1, y=>2, z=>3), though,*x+y*does have the value 3. By mapping strings in While into mathematical expressions (rather than values) we can use the algebra of the expressions to reason about*Aexp*s.##### Exercises on Semantics of Aexp

Exercise: Is*m*on*Aexp*a total function or a partial function? Is it a one-to-one function or many-to-one function? If it is one to one prove that it, otherwise find a equivalence relation so that semantically equivalent Aexp's are equivalent.Exercise: How do you prove the following Aexp are equivalent?

- "(x+y)+z" equivalent "x+(y+x)"
Write down half a dozen similar properties of the arithmetic expressions of
While that must follow from this semantics and the definition of a ring.
Exercise: Do these semantics force the implementor to provide infinite precision arithmetic or not? Prove your claim.

##### Semantics of Bexp

- m::Bexp->Condition. A Condition is a relation on states that either fails or does nothing, see: [ Conditions ]
- m("true")::=Id,
- m("false")::={},
- For b1:Bexp, m("~" b1)::= no m(b1).
- For b1,b2,b:Bexp, o:pre(op), m(b1 o b2)::=m(b1) op(o) m(b2).
The Boolean operations (and,or) on predicates define conditions that are related to the set theoretic operators of intersection and union:

*{ s || P and Q} = {s||P} & {s||Q}*- and so to the
[ Calculus of Relations ]
I define

*m:(Aexp Op Aexp)->Condition*in terms of two auxiliary functions: - op::string->infix(Sets)= ("and"+>(and) | "or"+>(or) | ...) ,
- rel::string->@(number, number)=("<" +> (<) | "=" +> (=) | ...). that relate strings (in the syntactic domain) to operations in the semantic domains.
- For a1,a2:Aexp, R:pre(rel), m(a1 R a2)::=( m(a1) rel(R) m(a2)).
This definition constructs a predicate on the state, and this predicate defines the set of states that satisfy the relationship. The underlying formalism is described below: [ Dynamic Predicates ]

##### Example of Semantics of Bexp

Suppose Var={"x", "y" , "z" } then State = ${ x,y,z::number }, and a typical state would be*s=State(x=>1, y=>2, z=>3)*. The function*m:Var->{x,y,z}*then maps "x" into*x*, "y" into*y*, and "z" into*y*: - m= ("x"+>x | "y"+>y | "z"+> z)
- = {("x", x) , ("y", y), ( "z", z) }.
- :.
- m("x>y /\ z<2") = (m("x") >m("y")) and (m("z") < m("2") )
- = ( x>y and z <2 ).
So "x>y /\ z<2" means the relation that does not change states and where

*(x>y and x<2)*. So - m("x>y /\ z<2")= rel[s,s']( s=s' and s.x>y.x and s.z<2)
- = Id & {(s,s')|| s.x>s.y} & {(s,s')|| s.z<2}.
##### Exercises on Semantics of Bexp

Exercise: Is*m*on Bexp a total function or a partial function? Is it a one-to-one function or many-to-one function? If one to one prove that it, otherwise find a equivalence relation so that semantically equivalent Aexp's are equivalent.Exercise: Show that for all b, m(

*b*) is a Condition. Prove that it is there deterministic but not total. For which Bexp is m(b) a function? and which function is it?##### Relational Semantics of Stm

The following relational semantics of While is a natural and denotational semantics. The meaning of a statement is a relation that is defined to hold between*s*and*s'*precisely when the statement terminates in state*s'*when started in*s'*. It seems possible to develop a set of relational equations that define the*structural operational semantics*of a statement - where the relation holds between successive states as the program executes. To find out more see [ Structural Operational Semantics ] below. - For S:Stm, m(
*S*)::Change=*Statement S terminates in state (2nd) if started in state (1st)*. - For x:Var, a:Aexp, m(x ":=" a )::=(m(x)'=m(
*a*)), where x'=e is defined below: [ Dynamic Predicates ] - m("skip")::=Id.
- For S1,S2:Stm, m(S1";" S2)::= m(S1); m(S2).
- For b:Bexp, S1,S2:Stm, m("if" b "then" S1 "else" S2)::= m(b); m(S1) | no
m(b); m(S2).
- For b:Bexp, S:Stm, m("while" b "do" S)::= do( m(b); m(S) ); no(m("b")).
Notation:

*Id*,*;*,*|*,*do*,*no*,*;*, etc. are from the calculus of Relations, see [ Calculus of Relations ]Note. These form a compositional definition: the meaning of each statement is expressed in terms of the meanings of its components in the syntax. In other words the definition is driven by the structure of the data.

##### Example of Semantics of a Program

When Var={"x", "y" , "z" } and F="(z:=1; y:=x); while ( y > 1 ) do ( z:=z*y; y:=y-1 ))". So - |- State::= ${x,y,z::number.}.
- |-m(
*F*) = ( (z'=1; y'=x); do(y>1; (z'=z*y; y'=y-1)); no(y>1))).##### Exercises on the Relational Semantics of Aexp

Exercise: Is*m*on*Stm*a total function or a partial function? Is it a one-to-one function or many-to-one function? If many to one derive a congruence so that modulus the congruence semantically equivalent, , otherwise prove that the function is one-one.Exercise: Show that all assignments are Actions.

We say that a statement

*S*is deterministic if m(*S*) is a deterministic relation.Exercise: Show that

*x:=a*and*skip*are deterministic. Show that if the components of a sequence, selection, or iteration are deterministic then so are the compound statement.Exercise: From the previous exercise, can we deduce that all While programs are deterministic? Can you explain your answer? Can you present a formal proof of your answer?

Exercise(For Mathematicians) : In how many different senses is

*m*a homomorphism between two systems? Is it a isomorphism, monomorphism, homeomorphism, etc.Exercise(Advanced) : Suppose one started by defining

*m*as function mapping some strings into a family of disjoint meanings, as above. Further suppose that every partial definition is compositional. Show that a context free grammar can be deconstructed from the functions. Show that*m*is total on the language of your deconstructed grammar.*. . . . . . . . . ( end of section Semantic Equations)*<<Contents | Index>>*. . . . . . . . . ( end of section Syntax and Semantics)*<<Contents | Index>>### Conclusion

In the above collection of semantic equations*m*is nearly always distributed to all the parts of the construct being assigned a meaning. A few examples would show that every construct in*While*is mapped directly into a simple expression in the calculus of relations.I conclude that we could use the calculus of relations as our ultimate semantic metalanguage. I claim that, relations even form an uniquely interesting and powerful programming language of their own. They are interesting because they are the only piece of existing mathematics is already a programming language. They are powerful because they can express concurrency and non-determinism.

*. . . . . . . . . ( end of section Main Text)*<<Contents | Index>>## Footnotes

### XBNF

EBNF uses - term::=expression.
The general XBNF form is For

*D*,*term*(*p*)::*T*=*e*.where

*D*declares the names and types of the parameters*p*(if any) and*T*is the type. In theory however this is the same as*term*::*P*->*T*= fun[*D*](*e*).The notation

*term*::*T*associates a type with a term.*. . . . . . . . . ( end of section XBNF)*<<Contents | Index>>### Calculus of Relations

- Relations on a Set X::= @(X,X).
- Intension::= rel[x,y:X]( W(x,y) ), rel[x,y:X]( W(x,y) ) ::= { (x,y): X><X | W(x,y) }.
- Identity::= (Id = rel[x,y](x=y)).
- Null relation::= {}.
- Universal relation::= X><X.
- Conditions::=
*subsets of the Id relation*. - Union::= R | S.
- Intersection::= R & S.
- Composition::= R; S.
- Complement::= ~R.
- Opposite::=no(R) ::= rel[ x, y ]( for no z(x R z) and x=y).
- Condition::=A ::= rel[ x, y ]( x \in A and x=y), -- A is a Set X.
- Reflexive_Transitive_Closure::=do(R).
The defining property of

*do(R)*is a second order property that*x do(R) y*iff all invariant(or closed) sets under*R*that contain*x*also contain*y*. Whitehead & Russell Circa 1930For more information see: [ logic_41_HomogenRelations.html ]

(deterministic): A relation*R*is*deterministic*if for all*x*, there is no more than one*y*such that*x R y*.

(total): A relation*R*is*total*if for all*x*, there is at least one*y*such that*x R y*.For more information on the calculus of relations see [ Relations in math_10_STANDARD ]

*. . . . . . . . . ( end of section Calculus of Relations)*<<Contents | Index>>### State Space

The formal model usually presented of a variable is a function*s:Var->Val*for some set of values. Thus if*v:Var*then*s(v) \in Val*. I assume that there is a labeled Cartesian Product or tuple where each*v:Var*has an associated label*l*and if 's:State' then*s.l \in Val*indicates the value of*v*in state*s*. I claim that this is effectively a simple change of notation.The notation is described informally in [ intro_records.html ]

*. . . . . . . . . ( end of section State Space)*<<Contents | Index>>### Dynamic Predicates

A dynamic predicate is a predicate that contains constants and variables (labels) from the state space, where a predicate is a formula that is either true or false. One special notation is added: if a variable appears with a prime then that variable is said to be dynamic in that predicate and may change. Other variable in the predicate are said to be static and may not change. The occurrences of dynamic variables without a prime indicate the old values of the variable and the occurrences with a prime indicate the new values - values in the new state. For more see [ math_14_Dynamics.html ]#### Conditions as Static Predicates

When a predicate has no dynamic variables then it expresses a condition - a set of states that will not change, but can only be satisfied by some states and not others (in general). For example

*x+y>0*is satisfied by the set of states*{ s || s.x+s.y >0}*and defines the relationship*{ s,s' || s=s' and s.x+s.y >0}*.#### Assignments

The formula - (sample assignment): x'= e
is an example of a dynamic predicate that describes a change in variable
*x*with other variables being held constant. The new value of*x*is the value of the expression*e*using the old value of*x*. Or to be more precise:*e*is evaluated using values from the old state, and then the*x*component of the state is changed to the value of e.#### General Form

This section goes beyond the goal of expressing the semantics of a simple programming language.It is worth developing a theory of general dynamic predicates because they form a precise yet concise way of documenting and specifying code.

*. . . . . . . . . ( end of section Dynamic Predicates)*<<Contents | Index>>### CoProducts

In this document I define a function*m*piecemeal by giving a series of definitions each defined on a subset of the set of strings of characters. In traditional semantics a different symbol would be used for each case. Each piece of*m*however can have different type of codomain. For example, if the strings are divided into*A*s and*B*s then*m:A->X*and*m:B->Y*. To justify mathematically the abuse of notation of having a single symbol I have to argue that*m*is a well defined function from a domain to a (single) codomain. We know from Ada and C++ that a function can be overloaded unambiguously in this way... as long as*A*and*B*do not overlap. Since*A*and*B*are both sets of strings it is clear that there is a common domain*A|B*. However the two images of these sets*m(A)*,*m(B)*are different types of things - numbers vs sets of states for example. To maintain strong typing and allow the use of single symbol I suppose that for any pair of types*T1*and*T2*there exists a different type called the coproduct that a the theoretical model of the discriminated union (Ada), union(Algol 68 and C), or tagged record(Pascal). The theory of such coproducts is part of category theory. [ math_25_Categories.html ]*. . . . . . . . . ( end of section CoProducts)*<<Contents | Index>>### Structural Operational Semantics

Here I explore a less abstract and more detailed form of semantics. I want to see how a relation between successive states can be defined using the calculus of relations.Here a change is expressed in terms of a change in two components: the statement being executed and the state in which the execution starts. This is called a configuration and is written:

*(S,s)* - Configuration::=(Stm |{done}) >< State,
- Transition::=@(Configuration,Configuration).
The configurations of form

*( done, s)*are called terminal states and indicate that the program has terminated: - Terminal::={done}><State.
In texts

*(done, s)*is often written*s*. - For S:Stm, Next::Transition=
*In the first step of statement S, (1st) becomes (2nd)*. For x:Var, a:Aexp, s:State, (x ":=" a, s ) Next (done, m(x)'=m(*a*)),where x'=e is defined above: [ Dynamic Predicates ]

- For s:state, ("skip", s) Next (done, s).
For S1,S2,S3:Stm, s1,s2:State, if (S1, s1) Next (S3, s2) then (S1 ";" S2, s1) Next (S3 ";" S2, s2).

For b:Bexp, S1,S2:Stm, s1,s2:State, if m(b)=Id then ("if" b "then" S1 "else" S2, s1) Next (S1, s1). For b:Bexp, S1,S2:Stm, s1,s2:State, if m(b)={} then ("if" b "then" S1 "else" S2, s1) Next (S2, s1).

For b:Bexp, S:Stm, s:State, ("while" b "do" S, s) Next ("if" b "then" "(" S";" "while" b "do" S")" "else" "skip", s).

#### Exercise on Structural Operational Semantics

Prove that for all S:Stm, s1,s2:State, (S,s1) do(Next) (done, s2) iff s1 m(S) s2.Note: This is true for While, but is not true for some extensions of While.

It might be wondered why it is worth have a more complex and less abstract way of stating the semantics of a programming language. One reason is that Natural semantics can not express the idea of a single step in a program and so can not define the idea of interleaving the steps from two parallel programs.

An interesting question for further research is to find a set of compositional equations for the Next relation to replace the derivation rules for ";", "if", and "while".

- |-For all S, Next==> (1st'=1st";"S); Next; (1st'=1st";"S).
*. . . . . . . . . ( end of section Structural Operational Semantics)*<<Contents | Index>>*. . . . . . . . . ( end of section Footnotes)*<<Contents | Index>>*. . . . . . . . . ( end of section Relational Semantics of The While Language)*<<Contents | Index>>

(who is in fact quoting a medieval author refering to their reliance on the ancient philosophers like Aristotle!)

Natural operational semantics is defined by giving a set of derivation
rules and axioms for expressions written like this *< S, s > -> s*. The
formula means that the statement *S* in state *s* terminates and leaves the
system in state *s'*. The axioms and rules are not difficult to accept.
But they are not easy to reason with and are not compositional. On the
other hand denotational semantics gives a set of equations which define a
set of partial functions *D*\[*S*\] that map *s* into *s'*. Denotational
semantics uses from Dana Scott's work on complete partial orders and fixed
points. For more see
Nielsen and Nielsen 92

In my approach *Relational Semantics* you present a set of equations that
define a map from each statement *S* into a relationship between *s* and
*s'*. The equations define the relationship associated with *S* in terms of
the components of *S*. Thus we get a set of compositional equations for
the natural semantics. Indeed the equations are expressed in an extended
form of Backus-Naur-Form. To show this I define the syntax and semantics
the classic "While" Language used in all theoretical work and textbooks of
programming language semantics:
[ grammar_of_While ]

The set of relations on a set is a ready made domain or complete partial
ordered set in the following sense. First, the set of binary relations on
a set X is a partial order under inclusion(==>). The relations form a
*poset*
[ poset in math_21_Order ]
Second, there is a unique bottom and top element: the bottom(greatest lower
bound) of the poset is the null relation and the top(least upper bound) the
anything-to-anything relation. Finally, given any relation, R on X, the
Kleene sequence:

- 2 (Declaration)
- Action (Declaration)
- Aexp (Declaration)
- Aexp (Definition)
- assignment (Definition)
- Bexp (Declaration)
- Bexp (Definition)
- Change (Definition)
- Complement (Definition)
- Composition (Definition)
- Condition (Declaration)
- Condition (Definition)
- Conditions (Definition)
- Configuration (Definition)
- deterministic (Label)
- generator (Formula)
- grammar_of_While (Definition)
- Identity (Definition)
- Intension (Definition)
- Intersection (Definition)
- iteration (Definition)
- kleene (Formula)
- limit (Formula)
- loop (Definition)
- m (Declaration)
- m (Declaration)
- m (Declaration)
- m (Declaration)
- m (Function Declaration)
- m (Function Declaration)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- m (Function definition)
- number (Declaration)
- Num (Declaration)
- Num (Definition)
- op (Declaration)
- Opposite (Definition)
- Reflexive_Transitive_Closure (Definition)
- rel (Declaration)
- sample assignment (Formula)
- selection (Definition)
- sequence (Definition)
- State (Definition)
- Stm (Declaration)
- Stm (Definition)
- Terminal (Definition)
- term (Definition)
- total (Label)
- Transition (Definition)
- Union (Definition)
- Var (Declaration)