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 Enviornment */ Strand_Status := Active * env | Dead * env | Stablized * env env = variable → value Strand_Env = Strand_Status * id * commands /** Arithmetic & Relational Expressions Evaluation Functions**/ expr_value = Aexpr * env -> value rel_op = Rexpr * env -> value Global Enviornment: The ∪ character denotes a parallel construct that states that every stand environment runs in parallel with each other. ∪ (update(Γ(id),Γ)) id ∈ Strand_env Γ = id -> Strand_Env dom(Γ) = all active & Stablized strand environments newId = Γ * id -> id update: Strand_Env * Γ -> Γ' Rules (1) ------------------------------------------------------------- update(((Stabalized,env),id,comm),Γ) ⇓ Γ comm_eval((Active,env),comm,id,Γ) ⇓ (new_status,env',Γ') (2) ------------------------------------------------------------------- update(((Active,env),id,comm),Γ) ⇓ Γ'[(new_status,env')/id] comm_eval: Strand_Status * commands * id * Γ -> status * env * Γ' Rules (1) ------------------------------------------------------ comm_eval((s, env),stabalize,id,Γ) ⇓ (Stablized,env,Γ) (2) ------------------------------------------------------ comm_eval((s, env),die,id,Γ) ⇓ (Dead, env,Γ) expr_eval(e,env) ⇓ v (3) ---------------------------------------------------------- comm_eval((s,env),x:=e,id,Γ) ⇓ (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,id,Γ) ⇓ (s', env'',Γ'') rel_op(b, env) ⇓ true comm_eval((s, env),c1,id,Γ) ⇓ (s',env',Γ') (5) ------------------------------------------------------------------------- comm_eval((s, env),if b then c1 else c2,id,Γ) ⇓ (s', env',Γ') rel_op(b,env) ⇓ false comm_eval((s,env),c2,id,Γ) ⇓ (s', env',Γ') (6) ------------------------------------------------------------------------- comm_eval((s, env),if b then c1 else c2,id,Γ) ⇓ (s', env',Γ') newId(Γ,id) ⇓ id' (7) ----------------------------------------------- comm_eval((s,env),spawn,id,Γ) ⇓ (s,env,Γ)
Click to toggle
does not end with </html> tag
does not end with </body> tag
The output has ended thus: ---------------------------------------------- comm_eval((s,env),spawn,id,Γ) ⇓ (s,env,Γ)