Home My Page Projects Code Snippets Project Openings diderot
Summary Activity Tracker Tasks SCM

SCM Repository

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

View of /trunk/semantics/semantics

Parent Directory Parent Directory | Revision Log Revision Log


Revision 515 - (download) (annotate)
Wed Feb 9 19:57:05 2011 UTC (8 years, 5 months ago) by lamonts
File size: 3239 byte(s)
updated the global section in the semantics
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,Γ) 

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0