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 26 17:42:05 2011 UTC (10 years, 10 months ago) by lamonts
File size: 2819 byte(s)
`Fixed the structure of the semantics doc`
```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)  ------------------------------------------------------

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)

```