Diderot Formal Semantics =============================== variable ::= string id ::= integer Arithmetic expression (Aexp) e ::= n for n ∈ R | 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 * env | Dead * env | Stablized * env env = variable → value /** Global Environment Functions **/ Strand_Env = Strand_Status * id * commands * env Γ = id -> Strand_Env dom(Γ) = all Active & Stablized Strand Environments newId = Γ * id -> id /** Arithmetic & Relational Expressions Evaluation Functions**/ expr_value = Aexpr * env -> value rel_op = Rexpr * env -> value comm_eval: Strand_Status * commands -> status * env Rules (1) ------------------------------------------------------ comm_eval((s, env),stabalize) ⇓ (Stablized, env) (2) ------------------------------------------------------ comm_eval((s, env),die) ⇓ (Dead, env) expr_eval(e,env) ⇓ v (3) ---------------------------------------------------------- comm_eval((s,env),x:=e) ⇓ (s,env[x:=v]) comm_eval((s, env),c1) ⇓ (s', env') comm_eval((s', env),c2) ⇓ (s'',env'') (4) --------------------------------------------------------------------------------------- comm_eval((s, env),c1;c2) ⇓ (s', env'') rel_op(b, env) ⇓ true comm_eval((s, env),c1) ⇓ (s',env') (5) ------------------------------------------------------------------------- comm_eval((s, env),if b then c1 else c2) ⇓ (s', env') rel_op(b,env) ⇓ false comm_eval((s,env),c2) ⇓ (s', env') (6) ------------------------------------------------------------------------- comm_eval((s, env),if b then c1 else c2) ⇓ (s', env') update: Strand_Env -> Strand_Env Rules (1) ------------------------------------------------------------- update(((Stabalized,env),id,comm>)) ⇓ ((Stabalized,env),id,comm) comm_eval((Active,env),comm) ⇓ (new_status,env') (2) ------------------------------------------------------------- Update(((Active,env),_,comm>)) ⇓ ((new_status,env'),id,comm)
Click to toggle
does not end with </html> tag
does not end with </body> tag
The output has ended thus: ----------------------------- Update(((Active,env),_,comm>)) ⇓ ((new_status,env'),id,comm)