Go backward to Quantified Assignments
Go up to Top
Go forward to Initially-section
Assign-section
- List of program statements.
- Non-deterministic selection.
- Quantification possible.
- Examples:
- ([] i,j: 0 <=i<=N and 0 <=j<=N ::
U[i,j] := 0 if i!=j
~ 1 if i=j) - (|| i,j: 0 <=i<=N and 0 <=j<=N
and i!=j ::
U[i,j] := 0)
[] (|| i: 0 <=i<=N :: U[i,j] := 1) - ([] i: 0 <=i<=N :: U[i,j] := 1
[] (|| j: 0 <=j<=N and i!=j :: U[i,j]
:= 0) )
- Quantification condition must not depend on program variables.
- Numer of statements is fixed.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: intro.tex,v 1.2 1996/01/31 15:37:03 schreine Exp schreine