Commit f6862c01 authored by Clément Fumex's avatar Clément Fumex

Update doc with range types and float types, first go.

parent 4aa3615d
\begin{syntax} \begin{syntax}
module ::= "module" uident label* mdecl* "end" module ::= "module" uident-nq label* mdecl* "end"
\ \
mdecl ::= decl ; theory declaration mdecl ::= decl ; theory declaration
| "type" mtype-decl ("with" mtype-decl)* ; mutable types | "type" mtype-decl ("with" mtype-decl)* ; mutable types
| "type" lident ("'" lident)* invariant+ ; added invariant | "type" lident-nq ("'" lident-nq)* invariant+ ; added invariant
| "let" "ghost"? lident label* pgm-defn ; | "let" "ghost"? lident-nq label* pgm-defn ;
| "let" "rec" rec-defn ; | "let" "rec" rec-defn ;
| "val" "ghost"? lident label* pgm-decl ; | "val" "ghost"? lident-nq label* pgm-decl ;
| "exception" lident label* type? ; | "exception" lident-nq label* type? ;
| "namespace" "import"? uident mdecl* "end" ; | "namespace" "import"? uident-nq mdecl* "end" ;
\ \
mtype-decl ::= lident label* ("'" lident label*)* ; mtype-decl ::= lident-nq label* ("'" lident-nq label*)* ;
mtype-defn ; mtype-defn ;
\ \
mtype-defn ::= ; abstract type mtype-defn ::= ; abstract type
...@@ -19,7 +19,7 @@ ...@@ -19,7 +19,7 @@
| "=" "{" mrecord-field (";" mrecord-field)* "}" ; record type | "=" "{" mrecord-field (";" mrecord-field)* "}" ; record type
invariant* invariant*
\ \
mrecord-field ::= "ghost"? "mutable"? lident label* ":" type mrecord-field ::= "ghost"? "mutable"? lident-nq label* ":" type
\ \
pgm-defn ::= fun-body ; pgm-defn ::= fun-body ;
| "=" "fun" binder+ spec* "->" spec* expr ; | "=" "fun" binder+ spec* "->" spec* expr ;
......
...@@ -3,11 +3,21 @@ ...@@ -3,11 +3,21 @@
\ \
ualpha ::= "A"-"Z" ualpha ::= "A"-"Z"
\ \
alpha ::= lalpha | ualpha digit-or-us ::= "0"-"9" | "_"
\ \
lident ::= lalpha (alpha | digit | "'")* alpha-no-us ::= "a"-"z" | "A"-"Z"
\ \
uident ::= ualpha (alpha | digit | "'")* suffix ::= (alpha-no-us | "'"* digit-or-us)* "\"*
\
lident-nq ::= lalpha suffix
\
uident-nq ::= ualpha suffix
\
lident ::= lident ("'" alpha-no-us suffix)+
\
uident ::= uident ("'" alpha-no-us suffix)+
\
ident-nq ::= lident-nq | uident-nq
\ \
ident ::= lident | uident ident ::= lident | uident
\ \
......
...@@ -115,6 +115,96 @@ Note that the syntax for type ...@@ -115,6 +115,96 @@ Note that the syntax for type
expressions notably differs from the usual ML syntax (\eg the expressions notably differs from the usual ML syntax (\eg the
type of polymorphic lists is written \texttt{list 'a}, not \texttt{'a list}). type of polymorphic lists is written \texttt{list 'a}, not \texttt{'a list}).
\subsubsection{Algebraic types}
TO BE COMPLETED
\subsubsection{Record types}
TO BE COMPLETED
\subsubsection{Range types}
A declaration of the form \texttt{type r = < range \textit{a b} >}
defines a type that projects into the integer range
\texttt{[\textit{a,b}]}. Note that in order to make such a declaration
the theory \texttt{int.Int} must be imported.
Why3 let you cast an integer literal in a range type
(e.g. \texttt{(42:r)}) and will check at typing that the literal is in
range. Defining such a range type $r$ automatically introduces the
following:
\begin{whycode}
function r'int r : int
constant r'maxInt : int
constant r'minInt : int
\end{whycode}
The function \texttt{r'int} projects a term of type \texttt{r} to its
integer value. The two constants represent the high bound and low
bound of the range respectively.
Unless specified otherwise with the meta \texttt{"keep:literal"} on
\texttt{r}, the transformation \emph{eliminate\_literal} introduces an
axiom
\begin{whycode}
axiom r'axiom : forall i:r. r'minInt <= r'int i <= r'maxInt
\end{whycode}
and replaces all casts of the form \texttt{(42:r)} with a constant and
an axiom as in:
\begin{whycode}
constant rliteral7 : r
axiom rliteral7_axiom : r'int rliteral7 = 42
\end{whycode}
This type is used in the standard library in the theories
\texttt{bv.BV8}, \texttt{bv.BV16}, \texttt{bv.BV32}, \texttt{bv.BV64}.
\subsubsection{floating point types}
A declaration of the form \texttt{type f = < float \textit{eb sb} >}
defines the type of floating point numbers as specified by the
IEEE-754 standard. Here the literal \texttt{\textit{eb}} represents
the number of bits in the exponent and the literal
\texttt{\textit{sb}} the number of bits in the significand (including
the hidden bit). Note that in order to make such a declaration the
theory \texttt{real.Real} must be imported.
Why3 let you cast a real literal in a float type
(e.g. \texttt{(0.5:f)}) and will check at typing that the literal is
representable in the format. Note that Why3 do not implicitly round a
real literal when casting to a float type, it refuses the cast if the
literal is not representable.
Defining such a type \texttt{f} automatically introduces the following:
\begin{whycode}
predicate f'isFinite f
function f'real f : real
constant f'eb : int
constant f'sb : int
\end{whycode}
The predicate \texttt{f'isFinite} is the finitness predicate associated to
the float format. The function \texttt{f'real} projects a finite term of type
\texttt{f} to its real value, it is not specified for non finite terms.
Unless specified otherwise with the meta \texttt{"keep:literal"} on
\texttt{f}, the transformation \emph{eliminate\_literal} will
introduce an axiom
\begin{whycode}
axiom f'axiom :
forall x:f. f'isFinite x -> -. max_real <=. f'real x <=. max_real
\end{whycode}
where \texttt{max\_real} is the value of the biggest finite float in
the specified format. The transformation also replaces all casts of
the form \texttt{(0.5:f)} with a constant and an axiom as in:
\begin{whycode}
constant fliteral42 : f
axiom fliteral42_axiom : f'real fliteral42 = 0.5 /\ f'isFinite fliteral42
\end{whycode}
This type is used in the standard library in the theories
\texttt{ieee\_float.Float32} and \texttt{ieee\_float.Float64}.
\subsection{Formulas} \subsection{Formulas}
The syntax for formulas is given Figure~\ref{fig:bnf:formula}. The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
...@@ -288,7 +378,7 @@ right, lazily. ...@@ -288,7 +378,7 @@ right, lazily.
% \begin{flushleft}\ttfamily % \begin{flushleft}\ttfamily
% while $c$ do invariant \{ $I$ \} $e$ done % while $c$ do invariant \{ $I$ \} $e$ done
% \end{flushleft} % \end{flushleft}
% it iterates the loop body $e$ until the condition $c$ becomes false. % it iterates the loop body $e$ until the condition $c$ becomes false.
% \begin{eqnarray*} % \begin{eqnarray*}
% WP(\texttt{while} \ldots, Q) &=& I \land \\ % WP(\texttt{while} \ldots, Q) &=& I \land \\
% && \forall \vec{w} (c \land I \rightarrow WP(e,I)) \land (\neg c \land I \rightarrow Q) % && \forall \vec{w} (c \land I \rightarrow WP(e,I)) \land (\neg c \land I \rightarrow Q)
......
\begin{syntax} \begin{syntax}
theory ::= "theory" uident label* decl* "end" theory ::= "theory" uident-nq label* decl* "end"
\ \
decl ::= "type" type-decl ("with" type-decl)* ; decl ::= "type" type-decl ("with" type-decl)* ;
| "constant" constant-decl ; | "constant" constant-decl ;
...@@ -7,29 +7,29 @@ ...@@ -7,29 +7,29 @@
| "predicate" predicate-decl ("with" logic-decl)* ; | "predicate" predicate-decl ("with" logic-decl)* ;
| "inductive" inductive-decl ("with" inductive-decl)* ; | "inductive" inductive-decl ("with" inductive-decl)* ;
| "coinductive" inductive-decl ("with" inductive-decl)* ; | "coinductive" inductive-decl ("with" inductive-decl)* ;
| "axiom" ident ":" formula ; | "axiom" ident-nq ":" formula ;
| "lemma" ident ":" formula ; | "lemma" ident-nq ":" formula ;
| "goal" ident ":" formula ; | "goal" ident-nq ":" formula ;
| "use" imp-exp tqualid ("as" uident)? ; | "use" imp-exp tqualid ("as" uident)? ;
| "clone" imp-exp tqualid ("as" uident)? subst? ; | "clone" imp-exp tqualid ("as" uident)? subst? ;
| "namespace" "import"? uident decl* "end" ; | "namespace" "import"? uident-nq decl* "end" ;
\ \
logic-decl ::= function-decl ; logic-decl ::= function-decl ;
| predicate-decl | predicate-decl
\ \
constant-decl ::= lident label* ":" type ; constant-decl ::= lident-nq label* ":" type ;
| lident label* ":" type "=" term | lident-nq label* ":" type "=" term
\ \
function-decl ::= lident label* type-param* ":" type ; function-decl ::= lident-nq label* type-param* ":" type ;
| lident label* type-param* ":" type "=" term | lident-nq label* type-param* ":" type "=" term
\ \
predicate-decl ::= lident label* type-param* ; predicate-decl ::= lident-nq label* type-param* ;
| lident label* type-param* "=" formula | lident-nq label* type-param* "=" formula
\ \
inductive-decl ::= lident label* type-param* "=" ; inductive-decl ::= lident-nq label* type-param* "=" ;
"|"? ind-case ("|" ind-case)* ; "|"? ind-case ("|" ind-case)* ;
\ \
ind-case ::= ident label* ":" formula ; ind-case ::= ident-nq label* ":" formula ;
\ \
imp-exp ::= ("import" | "export")? imp-exp ::= ("import" | "export")?
\ \
...@@ -43,6 +43,6 @@ ...@@ -43,6 +43,6 @@
| "goal" qualid ; | "goal" qualid ;
\ \
tqualid ::= uident | ident ("." ident)* "." uident ; tqualid ::= uident | ident ("." ident)* "." uident ;
\ \
type-decl ::= lident label* ("'" lident label*)* type-defn; % type-decl ::= lident-nq label* ("'" lident-nq label*)* type-defn; %
\end{syntax} \end{syntax}
...@@ -3,5 +3,7 @@ ...@@ -3,5 +3,7 @@
| "'" lident ; type variable | "'" lident ; type variable
| "()" ; empty tuple type | "()" ; empty tuple type
| "(" type ("," type)+ ")" ; tuple type | "(" type ("," type)+ ")" ; tuple type
| "(" type ")" ; parentheses % | "(" type ")" ; parentheses
| "<" "range" integer integer ">" ; range type
| "<" "float" integer integer ">" ; float type %
\end{syntax} \end{syntax}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment