The heater example is not a very good example...

3 files changed, 151 insertions, 30 deletions

diff --git a/doc/readme.pdf b/doc/readme.pdf
index 89e5d4e..4c2482c 100644
--- a/doc/readme.pdf
+++ b/doc/readme.pdf
diff --git a/doc/readme.tm b/doc/readme.tm
index c6cde6d..c3fbafb 100644
--- a/doc/readme.tm
+++ b/doc/readme.tm
@@ -9,7 +9,7 @@
 
   Le projet consiste en la réalisation d'un analyseur statique pour des
   programmes SCADE, utilisant l'interprétation abstraite comme base de
-  travail. Les objectifs attendus sont :
+  travail. Les objectifs visés sont :
 
   <\itemize>
     <item>Preuve de propriétés de sûreté sur des programmes
@@ -17,6 +17,10 @@
     <item>Étude d'intervalles de variation pour des variables
   </itemize>
 
+  Nos travaux se placent dans la continuité de <cite|blanchetEtAl-PLDI03>,
+  <cite|cousotCousot79-1>, <cite|halbwachs94c>, <cite|lesartse>,
+  <cite|jhrsas99>.
+
   L'expérience a été menée sur un sous-ensemble très restreint du langage
   SCADE, comportant notamment :
 
@@ -32,6 +36,8 @@
     prises en compte)
   </itemize>
 
+  \;
+
   Dans ce document nous mettrons au clair les points suivants :
 
   <\enumerate>
@@ -59,6 +65,8 @@
 
   Par la suite, nous ne considérons que des programmes SCADE bien typés.
 
+  \;
+
   <section|Spécification>
 
   <subsection|Grammaire>
@@ -1111,8 +1119,8 @@
   Étant donné notre système représenté par une fonction de transition
   <math|f<rsup|#>> et une fonction de cycle <math|c<rsup|#>> (par facilité,
   on notera <math|g<rsup|#>=c<rsup|#>\<circ\>f<rsup|#>>), l'ensemble des
-  états accessible par le système est <math|S<rsup|#>=lfp<rsub|I<rsup|#>><around*|(|\<lambda\>s.I<rsup|#>\<sqcup\>g<rsup|#><around*|(|s|)>|)>>,
-  où <math|I<rsup|#>=<around*|\<llbracket\>|i|\<rrbracket\>><around*|(|\<top\>|)>>.
+  états accessible par le système est <math|S<rsup|#>=lfp<rsub|S<rsub|0><rsup|#>><around*|(|\<lambda\>s.S<rsub|0><rsup|#>\<sqcup\>g<rsup|#><around*|(|s|)>|)>>,
+  où <math|S<rsub|0><rsup|#>=<around*|\<llbracket\>|i|\<rrbracket\>><around*|(|\<top\>|)>>.
 
   Pour <math|d<rsub|0>\<in\>\<bbb-M\><rsub|d>>, notons
   <math|r<rsub|d<rsub|0>> : \<cal-D\><rsup|#>\<rightarrow\>\<cal-D\><rsup|#>>
@@ -1125,7 +1133,7 @@
     <item>Poser :
 
     <\eqnarray*>
-      <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
+      <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|S<rsub|0><rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
       s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|0>|}>>>>>
     </eqnarray*>
 
@@ -1150,7 +1158,7 @@
   et non par union simple dans le futur. La définition devient alors :
 
   <\eqnarray*>
-    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
+    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|S<rsub|0><rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
     s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|0>|}>>>|<row|<cell|K<rsub|\<nabla\>,0>>|<cell|=>|<cell|\<varnothing\>>>>>
   </eqnarray*>
 
@@ -1175,7 +1183,7 @@
   d'itération suivant :
 
   <\eqnarray*>
-    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|I<rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
+    <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|S<rsub|0><rsup|#>>>|<row|<cell|\<delta\><rsub|0>>|<cell|=>|<cell|<around*|{|d\<in\>\<bbb-M\><rsub|d>\|
     s<rsub|0><around*|(|d|)>\<neq\>\<bot\><rsub|0>|}>>>|<row|<cell|K<rsub|\<nabla\>,0>>|<cell|=>|<cell|\<varnothing\>>>>>
   </eqnarray*>
 
@@ -1407,7 +1415,7 @@
 
   <\eqnarray*>
     <tformat|<table|<row|<cell|s<rsub|0>>|<cell|=>|<cell|\<oast\><rsub|\<bot\>>
-    I<rsup|#>>>>>
+    S<rsub|0><rsup|#>>>>>
   </eqnarray*>
 
   (appliquer <math|\<oast\>> de la sorte permet de faire que toutes les
@@ -1445,9 +1453,9 @@
 
   <subsection|Partitionnement dynamique>
 
-  Une autre approche à base de partitionnement dynamique a été tentée (cf
-  <em|Dynamic Partitionning in Analyses of Numerical Properties>), mais elle
-  n'a pas donné de très bons résultats par manque d'une heuristique sur les
+  Une autre approche à base de partitionnement dynamique a été tentée (cette
+  approche est décrite dans <cite|jhrsas99>)<math|>, mais elle n'a pas donné
+  de très bons résultats par manque d'une heuristique sur les
   partitionnements à effectuer.
 
   L'idée de base consiste à se donner une liste de conditions
@@ -1509,10 +1517,10 @@
   suivants :
 
   <\itemize>
-    <item>parser, lexer, typeur pour notre sous-ensemble de SCADE (source des
-    fichiers dans <verbatim|frontend/>)
+    <item>lexer, parser, typeur symple pour notre sous-ensemble de SCADE
+    (source des fichiers dans <verbatim|frontend/>)
 
-    <item>interprète pour la sémantique cocnrète
+    <item>interprète pour la sémantique concrète
     (<verbatim|interpret/interpret.ml>)
 
     <item>implémentation de la transformation d'un programme en formule
@@ -1737,22 +1745,46 @@
     ...) que l'on exécuterait comme pré-processing sur le programme.
   </itemize>
 
-  <section*|Références>
-
-  <\itemize>
-    <item><name|N.Halbwachs>, <em|About synchronous programming and abstract
-    interpretation>, International Symposium on Static Analysis, SAS'94.
-
-    <item><name|N.Halbwachs>, <name|F.Lagnier> and <name|C.Ratel>,
-    <em|Programming and verifying real-time systems by means of the
-    synchronous data-flow programming language Lustre>, IEEE Transactions on
-    Software Engineering, Spcial Issue on the Specification and Analysis of
-    Real-Time Systems, Sept. 1992
-
-    <item><name|B.Jeannet>, <name|N.Halbwachs> and <name|P.Raymond>,
-    <em|Dynamic Partitioning in Analyses of Numerical Properties>, Static
-    Analysis Symposium, SAS'99.
-  </itemize>
+  <\bibliography|bib|tm-plain|research.bib>
+    <\bib-list|5>
+      <bibitem*|1><label|bib-blanchetEtAl-PLDI03>B.<nbsp>Blanchet,
+      P.<nbsp>Cousot, R.<nbsp>Cousot, J.<nbsp>Feret, L.<nbsp>Mauborgne,
+      A.<nbsp>Miné, D.<nbsp>Monniaux<localize| and >X.<nbsp>Rival.<newblock>
+      A static analyzer for large safety-critical software.<newblock>
+      <localize|In ><with|font-shape|italic|Proceedings of the ACM SIGPLAN
+      2003 Conference on Programming Language Design and Implementation
+      (PLDI'03)>, <localize|pages >196--207. San Diego, California, USA, June
+      7--14 2003. ACM Press.<newblock>
+
+      <bibitem*|2><label|bib-cousotCousot79-1>P.<nbsp>Cousot<localize| and
+      >R.<nbsp>Cousot.<newblock> Systematic design of program analysis
+      frameworks.<newblock> <localize|In ><with|font-shape|italic|Conference
+      Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles
+      of Programming Languages>, <localize|pages >269--282. San Antonio,
+      Texas, 1979. ACM Press, New York, NY.<newblock>
+
+      <bibitem*|3><label|bib-halbwachs94c>N.<nbsp>Halbwachs.<newblock> About
+      synchronous programming and abstract interpretation.<newblock>
+      <localize|In >B.<nbsp>LeCharlier<localize|, editor>,
+      <with|font-shape|italic|International Symposium on Static Analysis,
+      SAS'94>. Namur (belgium), September 1994. LNCS 864, Springer
+      Verlag.<newblock>
+
+      <bibitem*|4><label|bib-lesartse>N.<nbsp>Halbwachs,
+      F.<nbsp>Lagnier<localize| and >C.<nbsp>Ratel.<newblock> Programming and
+      verifying real-time systems by means of the synchronous data-flow
+      programming language lustre.<newblock> <with|font-shape|italic|IEEE
+      Transactions on Software Engineering, Special Issue on the
+      Specification and Analysis of Real-Time Systems>, , September
+      \ 1992.<newblock>
+
+      <bibitem*|5><label|bib-jhrsas99>B.<nbsp>Jeannet,
+      N.<nbsp>Halbwachs<localize| and >P.<nbsp>Raymond.<newblock> Dynamic
+      partitioning in analyses of numerical properties.<newblock>
+      <localize|In ><with|font-shape|italic|Static Analysis Symposium,
+      SAS'99>. Venezia (Italy), sep 1999.<newblock>
+    </bib-list>
+  </bibliography>
 
   \;
 </body>
@@ -1813,15 +1845,34 @@
     <associate|auto-50|<tuple|7.1|19>>
     <associate|auto-51|<tuple|7.2|20>>
     <associate|auto-52|<tuple|<with|mode|<quote|math>|\<bullet\>>|20>>
+    <associate|auto-53|<tuple|3|20>>
     <associate|auto-6|<tuple|2.3.1|3>>
     <associate|auto-7|<tuple|2.3.2|3>>
     <associate|auto-8|<tuple|2.3.3|3>>
     <associate|auto-9|<tuple|2.3.4|4>>
+    <associate|bib-blanchetEtAl-PLDI03|<tuple|1|?>>
+    <associate|bib-cousotCousot79-1|<tuple|2|?>>
+    <associate|bib-halbwachs94c|<tuple|3|?>>
+    <associate|bib-jhrsas99|<tuple|5|?>>
+    <associate|bib-lesartse|<tuple|4|?>>
   </collection>
 </references>
 
 <\auxiliary>
   <\collection>
+    <\associate|bib>
+      blanchetEtAl-PLDI03
+
+      cousotCousot79-1
+
+      halbwachs94c
+
+      lesartse
+
+      jhrsas99
+
+      jhrsas99
+    </associate>
     <\associate|toc>
       <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>Introduction>
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
@@ -2025,7 +2076,7 @@
       taille réelle \T <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
       <no-break><pageref|auto-51>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Références>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Bibliographie>
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
       <no-break><pageref|auto-52><vspace|0.5fn>
     </associate>
diff --git a/doc/research.bib b/doc/research.bib
new file mode 100644
index 0000000..dcf93bc
--- /dev/null
+++ b/doc/research.bib
@@ -0,0 +1,70 @@
+
+@INPROCEEDINGS{halbwachs94c,
+   AUTHOR={N. Halbwachs},
+   TITLE={About synchronous programming and abstract interpretation},
+   BOOKTITLE={International Symposium on Static Analysis, SAS'94},
+   EDITOR = {B. {LeCharlier}},
+   PUBLISHER = {LNCS 864, Springer Verlag},
+   ADDRESS = {Namur (belgium)},
+   MONTH = {September},
+   YEAR= 1994
+}
+@ARTICLE{lesartse,
+    AUTHOR = {N. Halbwachs and F. Lagnier and C. Ratel },
+    TITLE = {Programming and verifying real-time systems by means of 
+             the synchronous data-flow programming language Lustre},
+    JOURNAL = {IEEE Transactions on Software Engineering, 
+               Special Issue on the Specification and Analysis 
+               of Real-Time Systems},
+    MONTH={September },
+    YEAR=1992
+}
+@INPROCEEDINGS{jhrsas99,
+AUTHOR = {B. Jeannet and N. Halbwachs and P. Raymond},
+TITLE={Dynamic Partitioning in Analyses of Numerical
+Properties},
+BOOKTITLE={Static Analysis Symposium, SAS'99},
+address={Venezia (Italy)},
+month = sep,
+year=1999
+}
+
+\bibitem{cousotCousot79-1}
+P. Cousot and R. Cousot.
+\newblock Systematic design of program analysis frameworks.
+\newblock In \emph{Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT
+  Symposium on Principles of Programming Languages}, pages 269--282, San
+  Antonio, Texas, 1979. ACM Press, New York, NY, U.S.A.
+
+@inproceedings{cousotCousot79-1,
+   author =    {Cousot, P. and Cousot, R.},
+   title =     {Systematic design of program analysis frameworks},
+   pages =     {269--282},
+   booktitle = {Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT 
+                Symposium on Principles of Programming Languages},
+   address =   {San Antonio, Texas},
+   publisher = {ACM Press, New York, NY},
+   year =      1979,
+}
+
+
+\bibitem{blanchetEtAl-PLDI03}
+B{.} Blanchet, P{.} Cousot, R{.} Cousot, J{.} Feret, L{.} Mauborgne, A{.}
+   Min\'e, D{.} Monniaux, and X{.} Rival.  
+\newblock A Static Analyzer for Large Safety-Critical Software.
+\newblock \emph{Proc{.} ACM SIGPLAN 2003 Conference on Programming Language
+   Design and Implementation} (PLDI'03), San Diego, California , USA, June
+   7--14, 2003, pp{.} 196--207.  ACM Press, 2003.
+
+@InProceedings{blanchetEtAl-PLDI03,
+   author =    {B. Blanchet and P. Cousot and  R. Cousot and J. Feret and
+                L. Mauborgne and A. Min\'e and D. Monniaux and X. Rival},
+   title =     {A Static Analyzer for Large Safety-Critical Software},
+   pages =     {196--207},
+   booktitle = {Proceedings of the ACM SIGPLAN 2003 Conference on Programming
+                Language Design and Implementation (PLDI'03)},
+   address =   {San Diego, California, USA},
+   publisher = {ACM Press},
+   month =     {June 7--14},
+   year =      2003,
+}