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

SCM Repository

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

Diff of /trunk/semantics/semantics

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 490, Wed Jan 19 19:49:01 2011 UTC revision 492, Wed Jan 26 17:42:05 2011 UTC
# Line 5  Line 5 
5  id ::= integer  id ::= integer
6    
7  Arithmetic expression (Aexp)  Arithmetic expression (Aexp)
8  e ::=  n       for n ∈ R or n ∈ Z  e ::=  n       for n ∈ R
9       | x       for x = variable       | x       for x = variable
10       | e1 + e2 for e1,e2 ∈ Aexp, Aexp       | e1 + e2 for e1,e2 ∈ Aexp, Aexp
11       | e1 - e2 for e1,e2 ∈ Aexp, Aexp       | e1 - e2 for e1,e2 ∈ Aexp, Aexp
# Line 32  Line 32 
32  v := Num(n) | Bool(b) | String(s) | tensor...??  v := Num(n) | Bool(b) | String(s) | tensor...??
33    
34    
35  Strand_Status := Active | Dead | Stablized  Strand_Status := Active * env | Dead * env | Stablized * env
   
36  env = variable → value  env = variable → value
37  Σ = id -> Strand_Env  
38    /** Global Environment Functions **/
39  Strand_Env = Strand_Status * id * commands * env  Strand_Env = Strand_Status * id * commands * env
40    Γ = id -> Strand_Env  dom(Γ) = all Active & Stablized Strand Environments
41    newId = Γ * id -> id
42    
43    /** Arithmetic & Relational Expressions Evaluation Functions**/
44  expr_value = Aexpr * env -> value  expr_value = Aexpr * env -> value
45  rel_op = Rexpr * env -> value  rel_op = Rexpr * env -> value
46    
47    
48  comm_eval: status * commands * env -> status * env  comm_eval: Strand_Status * commands  -> status * env
 Rules  
49    
50    Rules
51  (1)  ------------------------------------------------------  (1)  ------------------------------------------------------
52          comm_eval(status,Stablized,env) ⇓ (Stablized,env)          comm_eval((s, env),stabalize) ⇓ (Stablized, env)
53    
54    
55    (2)  ------------------------------------------------------
56            comm_eval((s, env),die) ⇓ (Dead, env)
57    
58    
59                      expr_eval(e,env) ⇓ v                      expr_eval(e,env) ⇓ v
60  (2) ----------------------------------------------------------  (3) ----------------------------------------------------------
61          comm_eval(status,x:=e,env) ⇓ (status,env[x:=v])          comm_eval((s,env),x:=e) ⇓ (s,env[x:=v])
62    
           comm_eval(s,c1,env) ⇓ (s',env')   comm_eval(s',c2,env') ⇓ (s'',env'')  
 (3) -------------------------------------------------------------------------  
                    comm_eval(s,c1;c2,env) ⇓ (s'',env'')  
63    
64                    comm_eval((s, env),c1) ⇓ (s', env')   comm_eval((s', env),c2) ⇓ (s'',env'')
65    (4) ---------------------------------------------------------------------------------------
66                       comm_eval((s, env),c1;c2) ⇓ (s', env'')
67    
           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')  
68    
69            rel_op(b,env) ⇓ false   comm_eval(s,c2,env) ⇓ (s',env')                  rel_op(b, env) ⇓ true   comm_eval((s, env),c1) ⇓ (s',env')
70  (5) -------------------------------------------------------------------------  (5) -------------------------------------------------------------------------
71                     comm_eval(s,if b then c1 else c2,env) ⇓ (s',env')                     comm_eval((s, env),if b then c1 else c2) ⇓ (s', env')
72    
73    
74                    rel_op(b,env) ⇓ false   comm_eval((s,env),c2) ⇓ (s', env')
75    (6) -------------------------------------------------------------------------
76                       comm_eval((s, env),if b then c1 else c2) ⇓ (s', env')
77    
78    
79    
80  update: Strand_Env -> Strand_Env  update: Strand_Env -> Strand_Env
81  Rules  Rules
 (1) -------------------------------------------------------------  
      update(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env>  
82    
83    (1) -------------------------------------------------------------
84         update(((Stabalized,env),id,comm>)) ⇓ ((Stabalized,env),id,comm)
85    
 (2)     (Doubt this will ever happen...?)  
     -------------------------------------------------------------  
            Update(<Dead,id,comm,env>) ⇓ <Dead,id,comm,env>  
86    
87                                   comm_eval(Comm,env) ⇓ <new_status,env'>                  comm_eval((Active,env),comm) ⇓ (new_status,env')
88  (3)  -------------------------------------------------------------  (2)  -------------------------------------------------------------
89          Update(<Active,_,x:=e,env>) ⇓ <new_status,id,comm,env'>          Update(((Active,env),_,comm>)) ⇓ ((new_status,env'),id,comm)
90    

Legend:
Removed from v.490  
changed lines
  Added in v.492

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