123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206 |
- \documentclass[11pt]{article}
- \usepackage{fullpage}
- %% Corrige quelques erreurs de LaTeX2ε
- \usepackage{fixltx2e}
- \usepackage{xspace}
- \usepackage{microtype}
- %% Pour ne pas commettre les erreurs fréquentes décrites dans l2tabu
- \usepackage[l2tabu,abort]{nag}
- %% Saisie en UTF-8
- \usepackage[utf8]{inputenc}
- %% Fonte : cf. http://www.tug.dk/FontCatalogue/
- \usepackage[T1]{fontenc}
- \usepackage{lmodern}
- %% Pour écrire du français
- % \usepackage[frenchb]{babel}
- %% Pour composer des mathématiques
- \usepackage{mathtools}
- \usepackage{amsfonts}
- \usepackage{amssymb}
- \usepackage{amsthm}
- \usepackage{stmaryrd}
- \usepackage{semantic}
- %% Commandes du paquet semantic : langage While
- \reservestyle{\command}{\textbf}
- \command{skip,while,do,if,then,else,not,and,or,true,false,int}
- %% -> Utiliser \<begin> Pour styliser le mot-clé
- \newcommand{\reduce}{\rightarrow^{*}}
- \begin{document}
- \author{Timoth\'ee Haudebourg \and Thibaut Marty}
- \title{Homework PAS/SDL}
- \date{November 18, 2016}
- \maketitle
- \section{Exercise 1}
- \subsection{Domains}
- The $State$ domain of evaluation is defined as:
- \[State = (Var \rightharpoonup Value) \cup \bot\]
- Where $Var$ is the set of variables, and $Value$ the set of possible values.
- We use $\bot$ to represent the error state.
- In our model, a record is represented as a partial application $Field \rightharpoonup Value$.
- This means that a record field can contains a record itself.
- To do so, we define the set of value as:
- \begin{align*}
- Value &= \bigcup_{i\in\mathbb{N}} Value_i \\
- Value_n &= \mathbb{N} \cup (Field \rightharpoonup Value_{n+1}) \\
- \end{align*}
- \subsection{Denotational Semantic for expressions}
- We define $\mathcal{A}$ the denotational semantics of arithmetic expressions as:
- \[ \mathcal{A}|[ \bullet |] : AExpr \rightarrow State \rightarrow (Value \cup \bot) \]
- where
- \begin{align*}
- \mathcal{A} |[ n |] \sigma &= \mathcal{N} |[n|] \\
- \mathcal{A} |[ x |] \sigma &= \sigma x \\
- \mathcal{A} |[ e_1\ o\ e_2 |] \sigma &= \mathcal{A} |[ e_1 |] \sigma\ \bar{o}\ \mathcal{A} |[ e_2 |] \sigma \\
- \mathcal{A} |[ e.f |] \sigma &= \mathcal{A}|[e|] \sigma f\\
- \mathcal{A} |[ e_1{f \mapsto e_2} |] \sigma f &= \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |] \sigma ]\\
- \mathcal{A} |[ \{f_1 = e_1 ; \dots ; f_n = e_n\} |] \sigma f_i &= \mathcal{A}|[ e_i |] \sigma \\
- \end{align*}
- For the undefined cases, for example when we try to add two records, we also note $\mathcal{A}|[e|] \sigma = \bot$.
- In the rest of this homwork, we suppose $\mathcal{B}|[ \bullet |]$ the denotational semantic for booleans expressions already defined.
- % TODO fin de la question : explications
- \subsection{Structural Operational Semantic for commands}
- We define $->$ the structural operational semantics for commands as:
- \[ -> : (Statement \times State) \times ((Statement \times State) \cup State) \]
- \subsubsection{Regular execution}
- For all $\sigma \neq \bot$:
- \[
- \inference{}{(skip, \sigma) -> \sigma}
- \]
- \[
- \inference{}{(x := a, \sigma) -> \sigma[x \mapsto \mathcal{A}|[a|] \sigma]}{\text{if }\mathcal{A}|[a|] \sigma \neq \bot}
- \]
- \[
- \inference{(S_1, \sigma) -> (S_1', \sigma')}{(S_1 ; S_2, \sigma) -> (S_1' ; S_2, \sigma')}
- \]
- \[
- \inference{(S_1, \sigma) -> \sigma'}{(S_1 ; S_2, \sigma) -> (S_2, \sigma')}
- \]
- \[
- \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> (S ; \<while>\ b\ \<do>\ S, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{tt}}
- \]
- \[
- \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{ff}}
- \]
- \[
- \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_1, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{tt}}
- \]
- \[
- \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> (S_2, \sigma)}{\text{if } \mathcal{B}|[b|] \sigma = \text{ff}}
- \]
- \subsubsection{Error handling}
- An error can occurs when one tries to add (or compare) records.
- In that case, according to our definition of arithmetic expressions, $\mathcal{A}|[e|] \sigma$ (or $\mathcal{B}|[b|]$) will returns $\bot$.
- From this point, the execution of the program makes no sense, and we will return the error state.
- \[
- \inference{}{(x := a, \sigma) -> \bot}{\text{if }\mathcal{A}|[a|] \sigma = \bot}
- \]
- \[
- \inference{}{(\<while>\ b\ \<do>\ S, \sigma) -> \bot}{\text{if } \mathcal{B}|[b|] \sigma = \bot}
- \]
- \[
- \inference{}{(\<if>\ b\ \<then>\ S_1\ \<else>\ S_2, \sigma) -> \bot}{\text{if } \mathcal{B}|[b|] \sigma = \bot}
- \]
- To ensure that the error can make it through the end, we also add the error propagation rule:
- \[
- \inference{}{(S, \bot) -> \bot}
- \]
- \section{Type system}
- We suppose now that every variable in the program is declared with a type satisfying the following syntax:
- \[
- t\quad::=\quad\text{int }|\ \{f_1 : t_1;\ \dots\ ; f_n : t_n\}
- \]
- We note $\Gamma \vdash S$ the type judgment for our language, defined by the following typing rules:
- \[
- \inference{}{\Gamma \vdash n : int}
- \]
- \[
- \inference{(x : T) \in \Gamma}{\Gamma \vdash x : T}
- \]
- \[
- \inference{\Gamma \vdash a_1 : int & \Gamma \vdash a_2 : int}{\Gamma \vdash a_1\ o\ a_2 : int}
- \]
- \[
- \inference{\Gamma \vdash e_1 : T_1 & \dots & \Gamma \vdash e_n : T_n}{\Gamma \vdash \{f_1 = e_1 ; \dots ; f_n = e_n\} : \{f_1 : T_1 ; \dots f_n : T_n\}}
- \]
- \[
- \inference{\Gamma \vdash \{f : T\}}{\Gamma \vdash e.f : T}
- \]
- \[
- \inference{\Gamma \vdash e_2 : T & \Gamma \vdash e_1 : \{f_1 : T_1 ; \dots ; f_n : T_n\}}{\Gamma \vdash e_1[f \mapsto e_2] : \{f : T ; f_1 : T_1 ; \dots ; f_n : T_n\}}
- \]
- % TODO : règle sub-typing
- % TODO : booléens… (autre photo)
- \section{Static analysis}
- $RF : Lab -> Var -> \mathcal{P}(Field)$
- % TODO : définir init
- \[
- \inference{RF(l) \subseteq RF (init(S)) & RF \vdash (S, l) & RF(l) \subseteq RF(l')}{RF \vdash (\<while>\ [b]^l\ \<do>\ S, l')}
- \]
- \[
- \inference{RF(l) \subseteq RF(init(S_1)) & RF \vdash (S_1, l') \\ RF(l) \subseteq RF(init(S_2)) & RF \vdash (S_2, l')}{RF \vdash (\<if>\ [b]^l\ \<then>\ S_1\ \<else>\ S_2, l')}
- \]
- \[
- \inference{RF(l) \subseteq RF(l')}{RF \vdash ([skip]^l, l')}
- \]
- \[
- \inference{RF \vdash (S_1, init(S_2)) & RF \vdash (S_2, l')}{RF \vdash (S_1 ; S_2, l')}
- \]
- \[
- \inference{RF(l)[x \mapsto \{f_1, \dots, f_n\}] \subseteq RF(l')}{RF \vdash ([x := \{f_1 = e_1 ; \dots ; f_n = e_n\}]^l, l')}
- \]
- \[
- % TODO : il faudrait évaluer statiquement e_1 pour être moins pessimiste
- \inference{RF(l)[x \mapsto \{f\}] \subseteq RF(l')}{RF \vdash ([x := e_1[f \mapsto e_2]]^l, l')}
- \]
- % autres affectations
- \[
- \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := n]^l, l')}
- \]
- \[
- \inference{RF(l)[x \mapsto RF(l)(y)] \subseteq RF(l')}{RF \vdash ([x := y]^l, l')}
- \]
- \[
- \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e_1\ o\ e_2]^l, l')}
- \]
- \[
- \inference{RF(l)[x \mapsto \emptyset] \subseteq RF(l')}{RF \vdash ([x := e.f]^l, l')}
- \]
- \end{document}
|