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

SCM Repository

[diderot] Diff of /trunk/doc/semantics/semantics.tex
ViewVC logotype

Diff of /trunk/doc/semantics/semantics.tex

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

revision 708, Wed Mar 30 16:41:18 2011 UTC revision 709, Wed Mar 30 16:55:10 2011 UTC
# Line 1  Line 1 
1  \documentclass[11pt]{article}  \documentclass[11pt]{article}
2    
3  \usepackage{proof}  \input{defs}
4  \usepackage{amsmath}  
5  \usepackage{graphicx}  \usepackage{graphicx}
6  \usepackage{fullpage}  \usepackage{fullpage}
7  \usepackage{amsfonts}  \usepackage{amsfonts}
8    
9  \newcommand{\point}{\textbullet~}  
 \newcommand{\INFER}[2]{\begin{array}{c}\infer{#1}{#2}\end{array}}  
10    
11  \title{Diderot Formal Semantics}  \title{Diderot Formal Semantics}
12  \author {  \author {
# Line 34  Line 33 
33    
34  \noindent{}\point Values:  v := Num(n)  \textbar{}  Bool(b) \textbar{} String(s) \textbar{} tensor...?? \textbar{} vecs...??  \noindent{}\point Values:  v := Num(n)  \textbar{}  Bool(b) \textbar{} String(s) \textbar{} tensor...?? \textbar{} vecs...??
35    
  \vspace{12pt}  
 \noindent{}\point Arithmetic expression (Aexp):  
 \begin{displaymath}  
         \begin{array}{rclr}  
         \text{e} &  ::= & n &\text{for n} \in\mathbb{R}  \\  
                    & \mid & \text{x} &\text{for x = variable}  \\  
                    & \mid & \text{$e_1 $ + $ e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
                    & \mid & \text{$e_1 $ - $ e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
                    & \mid & \text{$e_1 $ * $ e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
                    & \mid & \text{$e_1 $ / $ e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
     \end{array}  
   \end{displaymath}  
   
 \noindent{}\point Relational expression (Rexp):  
 \begin{displaymath}  
         \begin{array}{rclr}  
         \text{r} &  ::=  &\text{true}  \\  
                    & \mid & \text{false} \\  
                    & \mid & \text{$e_1  ==  e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
                    & \mid & \text{$e_1   <  e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
                    & \mid & \text{$e_1   >  e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
                    & \mid & \text{$e_1  \leq  e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
                     & \mid & \text{$e_1 \geq  e_2 $}  &\text{for $e_1$, $e_2$} \in\text{Aexp} \\  
   
   
     \end{array}  
   \end{displaymath}  
   
36  \noindent{}\point Commands (Comms):  \noindent{}\point Commands (Comms):
37  \begin{displaymath}  \begin{displaymath}
38          \begin{array}{rclr}          \begin{array}{rclr}
# Line 117  Line 88 
88    
89  $ \INFER{comm\_eval((s,env),die,id,\Gamma)\Downarrow (Dead,env,\Gamma)}{}$  $ \INFER{comm\_eval((s,env),die,id,\Gamma)\Downarrow (Dead,env,\Gamma)}{}$
90  \vspace{24pt}  \vspace{24pt}
91     %$\INFER{comm\_eval((s,env),x:=e,id,\Gamma)\Downarrow (s,env[x:=v],\Gamma)}{\ExpEval{env}{e}{v}} $
 $ \INFER{comm\_eval((s,env),x:=e,id,\Gamma)\Downarrow (s,env[x:=v],\Gamma)}{expr\_eval(e,env) \Downarrow  v}$  
92  \vspace{24pt}  \vspace{24pt}
93    
94  $ \INFER{comm\_eval((s,env),c_1; c_2,id,\Gamma)\Downarrow (s',env'',\Gamma'')}  $ \INFER{comm\_eval((s,env),c_1; c_2,id,\Gamma)\Downarrow (s',env'',\Gamma'')}

Legend:
Removed from v.708  
changed lines
  Added in v.709

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