Home My Page Projects Code Snippets Project Openings diderot

SCM Repository

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

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

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