Home My Page Projects Code Snippets Project Openings diderot

# SCM Repository

[diderot] View of /trunk/semantics/semantics
 [diderot] / trunk / semantics / semantics

# View of /trunk/semantics/semantics

Wed Jan 19 19:49:01 2011 UTC (11 years, 5 months ago) by lamonts
File size: 2645 byte(s)
`Added the Commands and Update Rules to the semantics`
```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(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env>

(2)     (Doubt this will ever happen...?)
-------------------------------------------------------------