Commit 4718c650 authored by Julien Signoles's avatar Julien Signoles
Browse files

moving E-ACSL reference manual from trunk to plugins/e-acsl

parent f874a3ed
MAIN=main
DEPS_MODERN=macros_modern.tex eacslversion.tex biblio.bib \
intro_modern.tex speclang_modern.tex \
libraries_modern.tex concl_modern.tex changes_modern.tex \
term_modern.bnf binders_modern.bnf predicate_modern.bnf \
fn_behavior_modern.bnf oldandresult_modern.bnf \
loc_modern.bnf \
assertions_modern.bnf loops_modern.bnf st_contracts_modern.bnf \
logic_modern.bnf data_invariants_modern.bnf model_modern.bnf \
ghost_modern.bnf generalinvariants_modern.bnf iterator_modern.bnf \
bsearch.c bsearch2.c link.c
.PHONY: all e-acsl default
default: e-acsl.pdf
e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
all: e-acsl
LANGUAGE_VERSION=1.5-4+dev
EACSL_VERSION= 0.1+dev
EACSL_DIR=$(HOME)/plugins/e-acsl
DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
install: e-acsl-implementation.pdf e-acsl.pdf
cp -f $^ $(EACSL_DIR)/doc/manuals
cp -f e-acsl.pdf \
$(DISTRIB_DIR)/download/e-acsl/e-acsl-$(LANGUAGE_VERSION).pdf
cp -f e-acsl-implementation.pdf \
$(DISTRIB_DIR)/download/e-acsl/e-acsl-implementation-$(EACSL_VERSION).pdf
include support/MakeLaTeXModern
eacslversion.tex: Makefile
rm -f $@
echo '\\newcommand{\\eacslversion}{$(EACSL_VERSION)}' > $@
chmod a-w $@
%.1: %.mp
mpost -interaction=batchmode $<
%.mps: %.1
mv $< $@
%.pp: %.tex pp
./pp -utf8 $< > $@
%.pp: %.c pp
./pp -utf8 -c $< > $@
%.tex: %.ctex pp
rm -f $@
./pp $< > $@
chmod a-w $@
%.bnf: %.tex transf
rm -f $@
./transf $< > $@
chmod a-w $@
%_modern.bnf: %.tex transf
rm -f $@
./transf -modern $< > $@
chmod a-w $@
%.ml: %.mll
ocamllex $<
%.pdf: %.tex
pdflatex $*
makeindex $*
bibtex $*
pdflatex $*
pdflatex $*
%.cmo: %.ml
ocamlc -c $<
pp: pp.ml
ocamlopt -o $@ str.cmxa $^
transf: transf.cmo transfmain.cmo
ocamlc -o $@ $^
transfmain.cmo: transf.cmo
.PHONY: clean
clean:
rm -rf *~ *.aux *.log *.nav *.out *.snm *.toc *.lof *.pp *.bnf \
*.haux *.hbbl *.htoc \
*.cb *.cm? *.bbl *.blg *.idx *.ind *.ilg \
transf trans.ml pp.ml pp
# version WEB lie ce qui est implement
e-acsl-implementation.pdf: $(DEPS_MODERN)
e-acsl-implementation.tex: $(MAIN).tex Makefile
rm -f $@
sed -e '/PrintRemarks/s/%--//' $^ > $@
chmod a-w $@
# version WEB du langage E-ACSL
e-acsl.pdf: $(DEPS_MODERN)
e-acsl.tex: e-acsl-implementation.tex Makefile
rm -f $@
sed -e '/PrintImplementationRq/s/%--//' $^ > $@
chmod a-w $@
# version pour le goupe de travail E-ACSL
$(MAIN).pdf: $(DEPS_MODERN)
\begin{syntax}
compound-statement ::= "{" declaration* statement* assertion+ "}"
\
statement ::= assertion statement \
assertion ::= "/*@" "assert" pred ";" "*/" ;
| { "/*@" "for" id ("," id)* ":" "assert" pred ";" "*/" } ;
\end{syntax}
/*@ requires \valid(p+(0..1));
@ requires \valid(q);
@*/
void f(int *p, int *q) {
*p = 0;
*(p+1) = 1;
*q = 0;
L1: *p = 2;
*(p+1) = 3;
*q = 1;
L2:
/*@ assert (\at(*(p+\at(*q,L1)),Here) == 2); */
/*@ assert (\at(*(p+\at(*q,Here)),L1) == 1); */
return ;
}
@STRING{SV = {Springer}}
@STRING{LNCS = {Lecture Notes in Computer Science}}
@INPROCEEDINGS{jml,
author = {Gary T. Leavens and K. Rustan M. Leino and Erik Poll
and Clyde Ruby and Bart Jacobs},
title = {{JML}: notations and tools supporting detailed design in {Java}},
booktitle = {{OOPSLA} 2000 Companion, Minneapolis, Minnesota},
pages = {105--106},
year = 2000
}
@INPROCEEDINGS{chalin07,
author = {Patrice Chalin},
title = {A Sound Assertion Semantics for the Dependable Systems Evolution
Verifying Compiler},
booktitle = {Proceedings of the International Conference on Software
Engineering (ICSE'07)},
pages = {23-33},
year = 2007,
address = {Los Alamitos, CA, USA},
publisher = {IEEE Computer Society}
}
@INPROCEEDINGS{chalin05,
author = {Patrice Chalin},
title = {Reassessing {JML}'s Logical Foundation},
booktitle = {Proceedings of the 7th Workshop on Formal Techniques for
Java-like Programs (FTfJP'05)},
year = 2005,
address = {Glasgow, Scotland},
month = JUL
}
@manual{acsl,
title = {{ACSL, ANSI/ISO C Specification Language}},
author = {Patrick Baudin and Jean-Christophe Filliâtre and Claude Marché
and Benjamin Monate and Yannick Moy and Virgile Prevosto},
year = {2011},
month = feb,
note = {Vesion 1.5. \url{http://frama-c.com/acsl.html}},
}
@manual{acslimplem,
title = {{ACSL version 1.5, Implementation in Carbon-20110201}},
author = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and
Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
year = {2011},
month = feb,
note = {\url{http://frama-c.com/acsl.html}},
}
@manual{framac,
title = {Frama-C User Manual},
author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and
Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski},
year = {2011},
month = oct,
note = {\url{http://frama-c.com}},
}
@manual{eacsl-plugin,
title = {Frama-C's E-ACSL Plug-in},
author = {Julien Signoles},
year = {2012},
month = jan,
note = {\url{http://frama-c.com}},
}
@manual{value,
title = {Frama-C's value analysis plug-in},
author = {Pascal Cuoq and Virgile Prevosto},
year = {2011},
month = oct,
note = {\url{http://frama-c.com/value.html}},
}
@BOOK{KR88,
author = {Brian Kernighan and Dennis Ritchie},
title = {The C Programming Language (2nd Ed.)},
publisher = {Prentice-Hall},
year = 1988
}
@MANUAL{standardc99,
title = {The {ANSI C} standard ({C99})},
organization = {International Organization for Standardization ({ISO})},
key = {C99},
note = {\url{http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf}}
}
\begin{syntax}
binders ::= binder (, binder)* ;
\
binder ::= type-expr variable-ident;
(,variable-ident)*
\
type-expr ::= logic-type-expr | C-type-expr
\
logic-type-expr ::= built-in-logic-type ;
| id ; type id
\
built-in-logic-type ::= "boolean" | "integer" | { "real" }
\
variable-ident ::= id
| "*" variable-ident ;
| variable-ident "[]";
| "(" variable-ident ")"
\end{syntax}
/*@ requires n >= 0 && \valid(t+(0..n-1));
@ assigns \nothing;
@ ensures -1 <= \result <= n-1;
@ behavior success:
@ ensures \result >= 0 ==> t[\result] == v;
@ behavior failure:
@ assumes t_is_sorted : \forall integer k1, int k2;
@ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];
@ ensures \result == -1 ==>
@ \forall integer k; 0 <= k < n ==> t[k] != v;
@*/
int bsearch(double t[], int n, double v) {
int l = 0, u = n-1;
/*@ loop invariant 0 <= l && u <= n-1;
@ for failure: loop invariant
@ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
@*/
while (l <= u ) {
int m = l + (u-l)/2; // better than (l+u)/2
if (t[m] < v) l = m + 1;
else if (t[m] > v) u = m - 1;
else return m;
}
return -1;
}
/*@ requires n >= 0 && \valid(t+(0..n-1));
@ assigns \nothing;
@ ensures -1 <= \result <= n-1;
@ behavior success:
@ ensures \result >= 0 ==> t[\result] == v;
@ behavior failure:
@ assumes t_is_sorted : \forall integer k1, int k2;
@ 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];
@ ensures \result == -1 ==>
@ \forall integer k; 0 <= k < n ==> t[k] != v;
@*/
int bsearch(double t[], int n, double v) {
int l = 0, u = n-1;
/*@ assert 0 <= l && u <= n-1;
@ for failure: assert
@ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
@*/
while (l <= u ) {
int m = l + (u-l)/2; // better than (l+u)/2
if (t[m] < v) l = m + 1;
else if (t[m] > v) u = m - 1;
else return m;
/*@ assert 0 <= l && u <= n-1;
@ for failure: assert
@ \forall integer k; 0 <= k < n ==> t[k] == v ==> l <= k <= u;
@*/ ;
}
return -1;
}
\section{Changes}
\subsection{Version \version}
\subsection{Version 1.5-4}
\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}
\subsection{Version 1.5-3}
\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}
\subsection{Version 1.5-2}
\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}
\subsection{Version 1.5-1}
\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}
\subsection{Version 1.5-0}
\begin{itemize}
\item Initial version.
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\ifthenelse%
{\boolean{PrintImplementationRq}}%
{
\section{Changes in \eacsl implementation}
\subsection{Version \eacslversion}
\begin{itemize}
\item Implement bitwise complementation.
\end{itemize}
\subsection{Version 0.1}
\begin{itemize}
\item Initial version.
\end{itemize}
}%
{}
\chapter{Conclusion}
This document presents an Executable ANSI/ISO C Specification Language. It
provides a subset of \acsl~\cite{acsl} implemented~\cite{acslimplem} in the
\framac platform~\cite{framac} in which each construct may be evaluated at
runtime. The specification language described here is intented to evolve in the
future in two directions. First it is based on \acsl which is itself still
evolving. Second the considered subset of \acsl may also change.
\begin{syntax}
declaration ::= { "/*@" data-inv-decl "*/" }
\
{ data-inv-decl } ::= { data-invariant } | { type-invariant }
\
{ data-invariant } ::= { { inv-strength? } "global" "invariant" } ;
{ id ":" pred ";" }
\
{ type-invariant } ::= { { inv-strength? } "type" "invariant" };
{ id "(" C-type-expr id ")" "=" pred ";" }
\
{ inv-strength } ::= { "weak" } | { "strong" }
\end{syntax}
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
\newcommand{\eacslversion}{0.1+dev}
\begin{syntax}
[ function-contract ] ::= requires-clause*;
{ decreases-clause? } simple-clause*;
named-behavior* { completeness-clause* }
\
requires-clause ::= "requires" predicate ";"
\
{ decreases-clause } ::= { "decreases" term ("for" ident)? ";" }
\
[ simple-clause ] ::= { assigns-clause } | ensures-clause
\
{ assigns-clause } ::= { "assigns" locations ";" }
\
{ locations } ::= { location ("," location) * | "\nothing" }
\
ensures-clause ::= "ensures" predicate ";"
\
named-behavior ::= "behavior" id ":" behavior-body
\
behavior-body ::= assumes-clause* requires-clause* simple-clause*
\
assumes-clause ::= "assumes" predicate ";"
\
{ completeness-clause } ::= { "complete" "behaviors" (id (","id)*)? ";" } ;
| { "disjoint" "behaviors" (id (","id)*)? ";" }
\end{syntax}
% --------------------------------------------------------------------------
% --- LaTeX Class for Frama-C Books ---
% --------------------------------------------------------------------------
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
% --------------------------------------------------------------------------
% --- Base Class management ---
% --------------------------------------------------------------------------
\LoadClass[a4paper,11pt,twoside,openright]{report}
\DeclareOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
\DeclareOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
\ProcessOptions
\RequirePackage{fullpage}
\RequirePackage{hevea}
\RequirePackage{ifthen}
\RequirePackage[T1]{fontenc}
\RequirePackage[latin1]{inputenc}
\RequirePackage[a4paper,pdftex,pdfstartview=FitH]{hyperref}
\RequirePackage{amssymb}
\RequirePackage{xcolor}
\RequirePackage[pdftex]{graphicx}
\RequirePackage{xspace}
\RequirePackage{makeidx}
\RequirePackage[leftbars]{changebar}
\RequirePackage[english]{babel}
\RequirePackage{fancyhdr}
\RequirePackage{titlesec}
% --------------------------------------------------------------------------
% --- Page Layout ---
% --------------------------------------------------------------------------
\setlength{\voffset}{-6mm}
\setlength{\headsep}{8mm}
\setlength{\footskip}{21mm}
\setlength{\textheight}{238mm}
\setlength{\topmargin}{0mm}
\setlength{\textwidth}{155mm}
\setlength{\oddsidemargin}{2mm}
\setlength{\evensidemargin}{-2mm}
\setlength{\changebarsep}{0.5cm}
\setlength{\headheight}{13.6pt}
\def\put@bg(#1,#2)#3{\setlength\unitlength{1cm}%
\begin{picture}(0,0)(#1,#2)
\put(0,0){\includegraphics{#3}}
\end{picture}}
\fancypagestyle{plain}{%
\fancyfoot{}
\fancyhead{}
\fancyhead[LE]{\put@bg(2.4,27.425){frama-c-left.pdf}}
\fancyhead[LO]{\put@bg(2.7,27.425){frama-c-right.pdf}}
\fancyhead[CE]{\scriptsize\textsf{\leftmark}}
\fancyhead[CO]{\scriptsize\textsf{\rightmark}}
\fancyfoot[C]{\small\textsf{\thepage}}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
}
\fancypagestyle{blank}{%
\fancyfoot{}
\fancyhead{}
\fancyhead[LE]{\put@bg(2.4,27.425){frama-c-left.pdf}}
\fancyhead[LO]{\put@bg(2.7,27.425){frama-c-right.pdf}}
}
%% Redefinition of cleardoublepage for empty page being blank
\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
\hbox{}
\thispagestyle{#1}
\newpage
\fi\fi}
\def\cleardoublepage{\cleardoublepagewith{blank}}
\pagestyle{plain}
% --------------------------------------------------------------------------
% --- Cover Page ---
% --------------------------------------------------------------------------
\newcommand{\coverpage}[1]{%
\thispagestyle{empty}
\setlength\unitlength{1cm}
\begin{picture}(0,0)(3.27,26.75)
\put(0,0){\includegraphics{frama-c-cover.pdf}}
\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
\end{picture}
}
% --------------------------------------------------------------------------
% --- Title Page ---
% --------------------------------------------------------------------------
\renewenvironment{titlepage}%
{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
{\end{center}}
\renewcommand{\title}[2]{
\vspace{20mm}
{\Huge\bfseries #1}
\bigskip
{\LARGE #2}
\vspace{20mm}
}
\renewcommand{\author}[1]{
\vspace{20mm}
{#1}
\medskip
}
% --------------------------------------------------------------------------
% --- Sectionning ---
% --------------------------------------------------------------------------
\titleformat{\chapter}[display]{\Huge\raggedleft}%
{\huge\chaptertitlename\,\thechapter}{0.5em}{}
\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
[\vspace{-14pt}\rule{\textwidth}{0.1pt}\vspace{-8pt}]
\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
[\vspace{-8pt}]
% --------------------------------------------------------------------------
% --- Main Text Style ---
% --------------------------------------------------------------------------
%\raggedright
\setlength\parindent{0pt}
\setlength\parskip{1ex plus 0.3ex minus 0.2ex}
\newenvironment{warning}[1][Warning:]{\small\paragraph{#1}\itshape}{\vspace{\parskip}}
\def\FramaC{\textsf{Frama-C}\xspace}
% --------------------------------------------------------------------------
% --- Listings ---
% --------------------------------------------------------------------------
\RequirePackage{listings}
\lstdefinelanguage{ACSL}{%
morekeywords={assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
exit_behavior,ghost,global,inductive,integer,invariant,lemma,logic,loop,
model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
union,variant},
% otherkeywords={\\at,\\base_addr,\\block_length,\\false,\\fresh,\\from,
% \\initialized,\\lambda,\\let,\\match,\\max,\\nothing,\\null,
% \\numof,\\old,\\result,\\specified,\\strlen,\\sum,\\true,
% \\valid,\\valid_range},
keywordsprefix={\\},
alsoletter={\\},
morecomment=[l]{//}
}
\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
\definecolor{lstbg}{gray}{0.98}
\definecolor{lstfg}{gray}{0.10}
\definecolor{lstrule}{gray}{0.6}
\definecolor{lstnum}{gray}{0.4}
\definecolor{lsttxt}{rgb}{0.3,0.2,0.6}
\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}%{0.6,0.6,0.2}
\definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
\definecolor{lstfile}{gray}{0.85}