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 489, Wed Jan 19 17:13:29 2011 UTC revision 490, Wed Jan 19 19:49:01 2011 UTC
# Line 25  Line 25 
25  c ::=   x := e                           for x = variable, e ∈ Aexp  c ::=   x := e                           for x = variable, e ∈ Aexp
26            | c1; c2                               for c1,c2  ∈ Comm            | c1; c2                               for c1,c2  ∈ Comm
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
29    
30    
31  Values  Values
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 | Dead | Stablized
36    
37  env = variable → value  env = variable → value
38    Σ = id -> Strand_Env
39  Strand_Env = Strand_Status * id * commands * env  Strand_Env = Strand_Status * id * commands * env
40    expr_value = Aexpr * env -> value
41    rel_op = Rexpr * env -> value
42    
43    
44    comm_eval: status * commands * env -> status * env
45    Rules
46    
47    (1)  ------------------------------------------------------
48            comm_eval(status,Stablized,env) ⇓ (Stablized,env)
49    
50                        expr_eval(e,env) ⇓ v
51    (2) ----------------------------------------------------------
52            comm_eval(status,x:=e,env) ⇓ (status,env[x:=v])
53    
54              comm_eval(s,c1,env) ⇓ (s',env')   comm_eval(s',c2,env') ⇓ (s'',env'')
55    (3) -------------------------------------------------------------------------
56                       comm_eval(s,c1;c2,env) ⇓ (s'',env'')
57    
58    
59  Update: Strand_Env -> Strand_Env            rel_op(b,env) ⇓ true   comm_eval(s,c1,env) ⇓ (s',env')
60    (4) -------------------------------------------------------------------------
61                       comm_eval(s,if b then c1 else c2,env) ⇓ (s',env')
62    
63  Rules:            rel_op(b,env) ⇓ false   comm_eval(s,c2,env) ⇓ (s',env')
64    (5) -------------------------------------------------------------------------
65                       comm_eval(s,if b then c1 else c2,env) ⇓ (s',env')
66    
67    update: Strand_Env -> Strand_Env
68    Rules
69  (1) -------------------------------------------------------------  (1) -------------------------------------------------------------
70       Update(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env>       update(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env>
71    
72    
73  (2)     (Doubt this will ever happen...?)  (2)     (Doubt this will ever happen...?)
74      -------------------------------------------------------------      -------------------------------------------------------------
75             Update(<Dead,id,comm,env>) ⇓ <Dead,id,comm,env>             Update(<Dead,id,comm,env>) ⇓ <Dead,id,comm,env>
76    
77                                   Update(<Active,_,e,env>) ⇓ v                                   comm_eval(Comm,env) ⇓ <new_status,env'>
78  (3)  -------------------------------------------------------------  (3)  -------------------------------------------------------------
79          Update(<Active,_,x:=e,env>) ⇓ env[x:=v]          Update(<Active,_,x:=e,env>) ⇓ <new_status,id,comm,env'>
80    

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

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