Go backward to Assign-section
Go up to Top
Go forward to Always-section
Initially-section
- Syntax similar to assign-section.
- Initial values of some variables.
- Function of initial values of other variables.
- Set of equations must be proper:
- Variable appears at most once on a left side.
- No circular variable dependencies.
- Examples:
- initially N = 3
[] (|| k: 0<=k<N :: A[N-k] = k) - initially B[0] = 0 || N = 2 []
([] i: 0<i<=N ::
A[i] = B[i-1] [] B[i] =
A[i])
- Section defines initial condition:
- Replace || and [] by and.
- Replace (x = e_0 if b_0 ~ ... ~e_n if b_n)
by (b_0 => (x = e_0) and ... and (b_n
=> (x = e_n)).
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: intro.tex,v 1.2 1996/01/31 15:37:03 schreine Exp schreine