Go backward to Valuation Functions
Go up to Top
Go forward to Concurrency

Example

C_0 = if G_1 [] G_2 fi
G_1 = X >= 0 -> Y := 1
G_2 = X = 0 -> Y := 0

C[[C_0]]s = ...

Case: access [[X]] s = zero
...= { (true, s_1) } where
    s_1 = update [[Y]] one s

Case: access [[X]] s > zero
...= { (true, s_1), (true, s_2) } where
    s_1 = update [[Y]] one s
    s_2 = update [[Y]] zero s

Case: access [[X]] s < zero
...= { (false, s) }


Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: intro.tex,v 1.2 1996/01/31 15:37:03 schreine Exp schreine

Prev Up Next