Substitutions change the program state. As they do not have a value, we cannot execute them. Instead, we provide some examples and give the B representation instead.
Empty Assignment
lisb2B=> skip
skip
Assignments
lisb2B=> (assign :x 42)
x := 42
lisb2B=> (assign :x 42 :y 1337)
x,y := 42,1337
lisb2B=> (becomes-element-of [:x] nat-set))
x :: NAT
lisb2B=> (becomes-member [:x :y] (cartesian-product nat-set (range 1 10)))
x,y :: NAT*(1..pred(10))
lisb2B=> (becomes-such [:x :y] (= :x (inc :y)))
x,y : (x=succ(y))
lisb2B=> (<-- [:x :y] (op-call :foo :a 42))
x,y <-- foo(a, 42)
Composition
lisb2B=> (|| (assign :x 42) (assign :y 43) (assign :z 1337))
x := 42 || y := 43 || z := 1337
lisb2B=> (parallel-sub (assign :x 42) (assign :y 43) (assign :z 1337))
x := 42 || y := 43 || z := 1337
lisb2B=> (sequential-sub (assign :x 42) (assign :y 43) (assign :z 1337))
x := 42 ; y := 43 ; z := 1337
Choices, Bindings, ...
lisb2B=> (any [:x :y] (< min-int :x :y max-int) (assign :a :x :b :y))
ANY x,y WHERE MININT < x & x < y & y < MAXINT THEN a,b := x,y END
lisb2B=> (let-sub [:x 42 :y 1337] (assign :a :x :y 1337))
LET x,y BE x=42 & y=1337 IN a,y := x,1337 END
lisb2B=> (var-sub [:x] (assign :x 42) (assign :a :x))
VAR x IN x := 42 ; a := x END
lisb2B=> (pre (= :x 42) (assign :y 42))
PRE x=42 THEN y := 42 END
lisb2B=> (assert (= :x 42) (assign :y 42))
ASSERT x=42 THEN y := 42 END
lisb2B=> (choice (assign :x 42) (assign :y 42))
CHOICE x := 42 OR y := 42 END
lisb2B=> (if-sub (= :x 0) (assign :x 100))
IF x=0 THEN x := 100 END
lisb2B=> (if-sub (= :x 0) (assign :x 100) (assign :x (dec :x)))
IF x=0 THEN x := 100 ELSE x := pred(x) END
lisb2B=> (cond (= :x 0) (assign :x 1) (= :y 0) (assign :y 1))
IF x=0 THEN x := 1 ELSIF y=0 THEN y := 1 END
lisb2B=> (cond (= :x 0) (assign :x 1) (= :y 0) (assign :y 1) (assign :v "default"))
IF x=0 THEN x := 1 ELSIF y=0 THEN y := 1 ELSE v := "default" END
lisb2B=> (select (= :x 0) (assign :x 1) (= :y 0) (assign :y 1))
SELECT x=0 THEN x := 1 WHEN y=0 THEN y := 1 END
lisb2B=> (select (= :x 0) (assign :x 1) (= :y 0) (assign :y 1) (assign :v "default"))
SELECT x=0 THEN x := 1 WHEN y=0 THEN y := 1 ELSE v := "default" END
lisb2B=> (case :x 0 (assign :x 1) 1 (assign :y 1))
CASE x OF EITHER 0 THEN x := 1 OR 1 THEN y := 1 END END
lisb2B=> (case :x 0 (assign :x 1) 1 (assign :y 1) (assign :v "default"))
CASE x OF EITHER 0 THEN x := 1 OR 1 THEN y := 1 ELSE v := "default" END END