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

SCM Repository

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

Annotation of /trunk/semantics/semantics

Parent Directory Parent Directory | Revision Log Revision Log


Revision 490 - (view) (download)

1 : lamonts 489 Diderot Formal Semantics
2 :     ===============================
3 :    
4 :     variable ::= string
5 :     id ::= integer
6 :    
7 :     Arithmetic expression (Aexp)
8 :     e ::= n for n ∈ R or n ∈ Z
9 :     | x for x = variable
10 :     | e1 + e2 for e1,e2 ∈ Aexp, Aexp
11 :     | e1 - e2 for e1,e2 ∈ Aexp, Aexp
12 :     | e1 * e2 for e1,e2 ∈ Aexp, Aexp
13 :     | e1 / e2 for e1,e2 ∈ Aexp, Aexp
14 :    
15 :     Relational expression (Rexp)
16 :     b ::= true
17 :     | false
18 :     | e1 == e2 for e1,e2 ∈ Aexp, Aexp
19 : lamonts 490 | e1 < e2 for e1,e2 ∈ Aexp, Aexp
20 :     | e1 > e2 for e1,e2 ∈ Aexp, Aexp
21 : lamonts 489 | e1 <= e2 for e1,e2 ∈ Aexp, Aexp
22 :     | e1 >= e2 for e1,e2 ∈ Aexp, Aexp
23 :    
24 :     Commands (Comm)
25 :     c ::= x := e for x = variable, e ∈ Aexp
26 :     | c1; c2 for c1,c2 ∈ Comm
27 :     | if b then c1 else c2 for c1,c2 ∈ Comm and b ∈ Rexp
28 : lamonts 490 | stabalize
29 : lamonts 489
30 : lamonts 490
31 : lamonts 489 Values
32 :     v := Num(n) | Bool(b) | String(s) | tensor...??
33 :    
34 : lamonts 490
35 : lamonts 489 Strand_Status := Active | Dead | Stablized
36 : lamonts 490
37 : lamonts 489 env = variable → value
38 : lamonts 490 Σ = id -> Strand_Env
39 : lamonts 489 Strand_Env = Strand_Status * id * commands * env
40 : lamonts 490 expr_value = Aexpr * env -> value
41 :     rel_op = Rexpr * env -> value
42 : lamonts 489
43 :    
44 : lamonts 490 comm_eval: status * commands * env -> status * env
45 :     Rules
46 : lamonts 489
47 : lamonts 490 (1) ------------------------------------------------------
48 :     comm_eval(status,Stablized,env) ⇓ (Stablized,env)
49 : lamonts 489
50 : lamonts 490 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 :     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 :     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 : lamonts 489 (1) -------------------------------------------------------------
70 : lamonts 490 update(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env>
71 : lamonts 489
72 :    
73 :     (2) (Doubt this will ever happen...?)
74 :     -------------------------------------------------------------
75 :     Update(<Dead,id,comm,env>) ⇓ <Dead,id,comm,env>
76 :    
77 : lamonts 490 comm_eval(Comm,env) ⇓ <new_status,env'>
78 : lamonts 489 (3) -------------------------------------------------------------
79 : lamonts 490 Update(<Active,_,x:=e,env>) ⇓ <new_status,id,comm,env'>
80 : lamonts 489

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