changes_modern.tex 5.39 KB
Newer Older
1
2
\section{Changes}

3
4
\subsection*{Version \version}
\begin{itemize}
5
6
7
8
9
10
11
12
\item Update according to \acsl 1.14:
  \begin{itemize}
  \item \changeinsection{assertions}{add the keyword \texttt{check}}
  \end{itemize}
\end{itemize}

\subsection*{Version 1.13}
\begin{itemize}
Julien Signoles's avatar
Julien Signoles committed
13
14
15
16
17
18
19
20
\item Update according to \acsl 1.13:
  \begin{itemize}
  \item \changeinsection{locations}{add syntax for set membership}
  \end{itemize}
\end{itemize}

\subsection*{Version 1.12}
\begin{itemize}
21
22
23
24
25
26
\item Update according to \acsl 1.12:
  \begin{itemize}
  \item \changeinsection{locations}{add subsections for build-in lists}
  \item \changeinsection{statement_contract}{fix syntax rule for statement
    contracts in allowing completeness clauses}
  \item \changeinsection{memory}{add syntax for defining a set by giving
Andre Maroneze's avatar
Andre Maroneze committed
27
    explicitly its element}
28
29
30
31
32
  \item \changeinsection{typedpointers}{new section}
  \end{itemize}
\end{itemize}

\subsection*{Version 1.9}
33

Julien Signoles's avatar
Julien Signoles committed
34
\begin{itemize}
35
\item \changeinsection{alloc-dealloc}{new section}
Julien Signoles's avatar
Julien Signoles committed
36
\item Update according to \acsl 1.9.
Julien Signoles's avatar
Julien Signoles committed
37
38
\end{itemize}

39
\subsection*{Version 1.8}
Julien Signoles's avatar
Julien Signoles committed
40

Julien Signoles's avatar
Julien Signoles committed
41
\begin{itemize}
42
43
\item \changeinsection{locations}{fix example \ref{ex:tset}}
\item \changeinsection{pointers}{add grammar of memory-related terms and
44
  predicates}
Julien Signoles's avatar
Julien Signoles committed
45
46
\end{itemize}

47
\subsection*{Version 1.7}
Julien Signoles's avatar
Julien Signoles committed
48

49
\begin{itemize}
50
\item Update according to \acsl 1.7.
51
52
53
\item \changeinsection{separation}{no more absent}
\end{itemize}

54
\subsection*{Version 1.5-4}
55
56
57
58
59
60
61
62
63
64
65
66
67

\begin{itemize}
\item Fix typos.
\item \changeinsection{expressions}{fix syntax of guards in iterators}
\item \changeinsection{semantics}{fix definition of undefined terms and
  predicates}
\item \changeinsection{typing}{no user-defined types}
\item \changeinsection{builtinconstructs}{no more implementation issue for
  \lstinline|\\old|}
\item \changeinsection{at}{more restrictive scoping rule for label references 
in \lstinline|\\at|}
\end{itemize}

68
\subsection*{Version 1.5-3}
69
70
71
72
73
74
75
76
77
78
79
80

\begin{itemize}
\item Fix various typos.
\item Warn about features known to be difficult to implement.
\item \changeinsection{expressions}{fix semantics of ternary operator}
\item \changeinsection{expressions}{fix semantics of cast operator}
\item \changeinsection{expressions}{improve syntax of iterator quantifications}
\item \changeinsection{semantics}{improve and fix example \ref{ex:semantics}}
\item \changeinsection{loop_annot}{improve explanations about loop invariants}
\item \changeinsection{logicalstates}{add hybrid functions and predicates}
\end{itemize}

81
\subsection*{Version 1.5-2}
82
83
84
85
86
87
88
89
90
91
92
93

\begin{itemize}
\item \changeinsection{expressions}{remove laziness of operator
  \lstinline|<==>|}
\item \changeinsection{expressions}{restrict guarded quantifications to integer}
\item \changeinsection{expressions}{add iterator quantifications} 
\item \changeinsection{expressions}{extend unguarded quantifications to char}
\item \changeinsection{locations}{extend syntax of set comprehensions}
\item \changeinsection{loop_annot}{simplify explanations for loop invariants and
  add example.}
\end{itemize}

94
\subsection*{Version 1.5-1}
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113

\begin{itemize}
\item Fix many typos.
\item Highlight constructs with semantic changes in grammars.
\item Explain why unsupported features have been removed.
\item Indicate that experimental \acsl features are unsupported.
\item Add operations over memory like \lstinline|\valid|.
\item \changeinsection{expressions}{lazy operators \lstinline|&&|,
  \lstinline+||+, \lstinline|\^\^|, \lstinline|==>| and \lstinline|<==>|}
\item \changeinsection{expressions}{allow unguarded quantification over boolean}
\item \changeinsection{expressions}{revise syntax of \lstinline|\\exists|}
\item \changeinsection{semantics}{better semantics for undefinedness}
\item \changeinsection{locations}{revise syntax of set comprehensions}
\item \changeinsection{loop_annot}{add loop invariants, but they lose their
  inductive \acsl nature}
\item \changeinsection{generalmeasures}{add general measures for termination}
\item \changeinsection{specmodules}{add specification modules}
\end{itemize}

114
\subsection*{Version 1.5-0}
115
116
117
118
119
120
121
122
123
124

\begin{itemize}
\item Initial version.
\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\ifthenelse%
    {\boolean{PrintImplementationRq}}%
    {
125
\section{Changes in \eacsl Implementation}
126

127
\subsection*{Version Argon-18}
Julien Signoles's avatar
Julien Signoles committed
128

Julien Signoles's avatar
Julien Signoles committed
129
\begin{itemize}
130
131
\item \changeinsection{at}{support of \lstinline|\\at| on purely
logic variables}
Julien Signoles's avatar
Julien Signoles committed
132
133
134
135
136
137
\item \changeinsection{locations}{support of ranges in memory built-ins
  (e.g. \lstinline|\\valid| or \lstinline|\\initialized|)}
\end{itemize}

\subsection*{Version Chlorine-20180501}

Julien Signoles's avatar
Julien Signoles committed
138
\begin{itemize}
139
140
141
142
143
144
145
\item \changeinsection{expressions}{support of \lstinline|\\let| binding}
\end{itemize}

\subsection*{Version 0.5}

\begin{itemize}
\item \changeinsection{alloc-dealloc}{support of \lstinline|\\freeable|}
Julien Signoles's avatar
Julien Signoles committed
146
147
\end{itemize}

148
\subsection*{Version 0.3}
Julien Signoles's avatar
Julien Signoles committed
149
150
151
152
153

\begin{itemize}
\item \changeinsection{loop_annot}{support of loop invariant}
\end{itemize}

154
\subsection*{Version 0.2}
155
156

\begin{itemize}
157
158
159
160
161
162
\item \changeinsection{expressions}{support of bitwise complementation}
\item \changeinsection{memory}{support of \lstinline|\\valid|}
\item \changeinsection{memory}{support of \lstinline|\\block_length|}
\item \changeinsection{memory}{support of \lstinline|\\base_addr|}
\item \changeinsection{memory}{support of \lstinline|\\offset|}
\item \changeinsection{dangling}{support of \lstinline|\\initialized|}
163
164
\end{itemize}

165
\subsection*{Version 0.1}
166
167
168
169
170
171
172

\begin{itemize}
\item Initial version.
\end{itemize}

    }%
    {}