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 514, Tue Feb 8 22:54:00 2011 UTC revision 515, Wed Feb 9 19:57:05 2011 UTC
# Line 27  Line 27 
27       | if b then c1 else c2      for c1,c2  ∈ Comm and b  ∈ Rexp       | if b then c1 else c2      for c1,c2  ∈ Comm and b  ∈ Rexp
28       | stabalize       | stabalize
29    
   
30  Values  Values
31  v := Num(n) | Bool(b) | String(s) | tensor...??  v := Num(n) | Bool(b) | String(s) | tensor...??
32    
33    
34    /** Strand Enviornment */
35  Strand_Status := Active * env | Dead * env | Stablized * env  Strand_Status := Active * env | Dead * env | Stablized * env
36  env = variable → value  env = variable → value
37    Strand_Env = Strand_Status * id * commands
38    
39    
 /** Global Environment Functions **/  
 Strand_Env = Strand_Status * id * commands * env  
 Γ = id -> Strand_Env  dom(Γ) = all Active & Stablized Strand Environments  
 newId = Γ * id -> id  
40    
41  /** Arithmetic & Relational Expressions Evaluation Functions**/  /** Arithmetic & Relational Expressions Evaluation Functions**/
42  expr_value = Aexpr * env -> value  expr_value = Aexpr * env -> value
43  rel_op = Rexpr * env -> value  rel_op = Rexpr * env -> value
44    
45    
46  comm_eval: Strand_Status * commands  -> status * env  Global Enviornment:
47    The ∪ character denotes a parallel construct that states that every stand environment
48    runs in parallel with each other.
49    
50    ∪ (update(Γ(id),Γ))
51    
52    id ∈ Strand_env
53    Γ = id -> Strand_Env
54    dom(Γ) = all active & Stablized strand environments
55    newId = Γ * id -> id
56    
57    
58    update: Strand_Env * Γ ->  Γ'
59    Rules
60    (1) -------------------------------------------------------------
61            update(((Stabalized,env),id,comm),Γ) ⇓ Γ
62    
63    
64             comm_eval((Active,env),comm,id,Γ) ⇓ (new_status,env',Γ')
65    (2)   -------------------------------------------------------------------
66            update(((Active,env),id,comm),Γ) ⇓   Γ'[(new_status,env')/id]
67    
68    
69    
70    comm_eval: Strand_Status * commands * id * Γ   -> status * env * Γ'
71  Rules  Rules
72  (1)  ------------------------------------------------------  (1)  ------------------------------------------------------
73          comm_eval((s, env),stabalize) ⇓ (Stablized, env)          comm_eval((s, env),stabalize,id,Γ) ⇓ (Stablized,env,Γ)
74    
75    
76  (2)  ------------------------------------------------------  (2)  ------------------------------------------------------
77          comm_eval((s, env),die) ⇓ (Dead, env)          comm_eval((s, env),die,id,Γ) ⇓ (Dead, env,Γ)
78    
79    
80                      expr_eval(e,env) ⇓ v                      expr_eval(e,env) ⇓ v
81  (3) ----------------------------------------------------------  (3) ----------------------------------------------------------
82          comm_eval((s,env),x:=e) ⇓ (s,env[x:=v])          comm_eval((s,env),x:=e,id,Γ) ⇓ (s,env[x:=v],Γ)
83    
84    
85                  comm_eval((s, env),c1) ⇓ (s', env')   comm_eval((s', env),c2) ⇓ (s'',env'')           comm_eval((s, env),c1,Γ) ⇓ (s', env',Γ')   comm_eval((s', env),c2,Γ') ⇓ (s'',env'',Γ'')
86  (4) ---------------------------------------------------------------------------------------  (4) ----------------------------------------------------------------------------------------------
87                     comm_eval((s, env),c1;c2) ⇓ (s', env'')                     comm_eval((s, env),c1;c2,id,Γ) ⇓ (s', env'',Γ'')
88    
89    
90                  rel_op(b, env) ⇓ true   comm_eval((s, env),c1) ⇓ (s',env')          rel_op(b, env) ⇓ true   comm_eval((s, env),c1,id,Γ) ⇓ (s',env',Γ')
91  (5) -------------------------------------------------------------------------  (5) -------------------------------------------------------------------------
92                     comm_eval((s, env),if b then c1 else c2) ⇓ (s', env')              comm_eval((s, env),if b then c1 else c2,id,Γ) ⇓ (s', env',Γ')
93    
94    
95                  rel_op(b,env) ⇓ false   comm_eval((s,env),c2) ⇓ (s', env')          rel_op(b,env) ⇓ false   comm_eval((s,env),c2,id,Γ) ⇓ (s', env',Γ')
96  (6) -------------------------------------------------------------------------  (6) -------------------------------------------------------------------------
97                     comm_eval((s, env),if b then c1 else c2) ⇓ (s', env')              comm_eval((s, env),if b then c1 else c2,id,Γ) ⇓ (s', env',Γ')
   
   
   
 update: Strand_Env -> Strand_Env  
 Rules  
   
 (1) -------------------------------------------------------------  
      update(((Stabalized,env),id,comm>)) ⇓ ((Stabalized,env),id,comm)  
   
98    
                 comm_eval((Active,env),comm) ⇓ (new_status,env')  
 (2)  -------------------------------------------------------------  
         Update(((Active,env),_,comm>)) ⇓ ((new_status,env'),id,comm)  
99    
100                      newId(Γ,id) ⇓ id'
101    (7) -----------------------------------------------
102            comm_eval((s,env),spawn,id,Γ) ⇓ (s,env,Γ)

Legend:
Removed from v.514  
changed lines
  Added in v.515

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