Diderot Formal Semantics =============================== variable ::= string id ::= integer Arithmetic expression (Aexp) e ::= n for n ∈ R or n ∈ Z | x for x = variable | e1 + e2 for e1,e2 ∈ Aexp, Aexp | e1 - e2 for e1,e2 ∈ Aexp, Aexp | e1 * e2 for e1,e2 ∈ Aexp, Aexp | e1 / e2 for e1,e2 ∈ Aexp, Aexp Relational expression (Rexp) b ::= true | false | e1 == e2 for e1,e2 ∈ Aexp, Aexp | e1 < e2 for e1,e2 ∈ Aexp, Aexp | e1 > e2 for e1,e2 ∈ Aexp, Aexp | e1 <= e2 for e1,e2 ∈ Aexp, Aexp | e1 >= e2 for e1,e2 ∈ Aexp, Aexp Commands (Comm) c ::= x := e for x = variable, e ∈ Aexp | c1; c2 for c1,c2 ∈ Comm | if b then c1 else c2 for c1,c2 ∈ Comm and b ∈ Rexp | stabalize Values v := Num(n) | Bool(b) | String(s) | tensor...?? Strand_Status := Active | Dead | Stablized env = variable → value Σ = id -> Strand_Env Strand_Env = Strand_Status * id * commands * env expr_value = Aexpr * env -> value rel_op = Rexpr * env -> value comm_eval: status * commands * env -> status * env Rules (1) ------------------------------------------------------ comm_eval(status,Stablized,env) ⇓ (Stablized,env) expr_eval(e,env) ⇓ v (2) ---------------------------------------------------------- comm_eval(status,x:=e,env) ⇓ (status,env[x:=v]) comm_eval(s,c1,env) ⇓ (s',env') comm_eval(s',c2,env') ⇓ (s'',env'') (3) ------------------------------------------------------------------------- comm_eval(s,c1;c2,env) ⇓ (s'',env'') rel_op(b,env) ⇓ true comm_eval(s,c1,env) ⇓ (s',env') (4) ------------------------------------------------------------------------- comm_eval(s,if b then c1 else c2,env) ⇓ (s',env') rel_op(b,env) ⇓ false comm_eval(s,c2,env) ⇓ (s',env') (5) ------------------------------------------------------------------------- comm_eval(s,if b then c1 else c2,env) ⇓ (s',env') update: Strand_Env -> Strand_Env Rules (1) ------------------------------------------------------------- update() ⇓ (2) (Doubt this will ever happen...?) ------------------------------------------------------------- Update() ⇓ comm_eval(Comm,env) ⇓ (3) ------------------------------------------------------------- Update() ⇓
Click to toggle
does not end with </html> tag
does not end with </body> tag
The output has ended thus: ---------------------------------- Update(<Active,_,x:=e,env>) ⇓ <new_status,id,comm,env'>