Skip to content

GitLab

why3
why3
Commit 6bb5875d authored by Johannes Kanig's avatar Johannes Kanig
Browse files
Options

Merge branch 'lri-master' into why3server

parents d7a2b1a7 4022988c
Hide whitespace changes
Inline Side-by-side
Showing with 3585 additions and 3031 deletions
CHANGES
View file @ 6bb5875d
* marks an incompatible change
Tools
o why3 config now generates default proof strategies using the
installed provers. These are available under name "Auto level 1"
and "Auto level 2" in why3 ide.
Version 0.87.0, March 15, 2016
================================
......
ROADMAP
View file @ 6bb5875d
......@@ -147,13 +147,12 @@ and no epsilon
chaque instance necessaires. plutot qu'un seul symbole _match
polymorphe.
==================== Roadmap for release 0.87 ========================
DATE : ?
==================== Roadmap for release 0.88 ========================
Release Notes (details in file CHANGES):
DATE : au plus tard en novembre 2016, pour que ce soit dispo pour les
etudiants MPRI (pour la feature strategies en particulier)
== TODO ==
* integrate server feature done by Johannes
* Document src/core/trans.mli, and fill the paragraph on
transformations in the tutorial: doc/api.tex, section 4.7 "Applying
......@@ -164,30 +163,15 @@ Release Notes (details in file CHANGES):
solution possible: symbol builtin t_neq, inlining systematique au typage
(ou laisser inline_trivial le faire)
* DONE finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
C'est finalisé. Mais les tuples restent polymorphes.
* integrate server feature done by Johannes
* DONE Coq realization of bitvector theory
* make counter-examples feature more robust
* DONE support for both isabelle 2014 and 2015
+ bugfix for installation
* DONE review support for division operators by SMT provers
* take some time to fix some bugs of the BTS: 18029 at least
* use the file generated by altgr-ergo to replay proofs edited by altgr-ergo
alt-ergo -replay <file>.agr
-> on pourrait le faire en considerant altgr-ergo comme un prouveur interactif
* make the strategy feature public and documented. Possibly generate
* DONE make the strategy feature public and documented. Possibly generate
default strategies dynamically at the time of why3 config --detect,
using the provers detected : for that, we can annotated the provers in
prover-detection-data.conf to tell if they should be used in the strategies,
......@@ -201,6 +185,27 @@ Release Notes (details in file CHANGES):
. or, favor timelimit increase...
* take some time to fix some bugs of the BTS: 18029 at least
==================== Roadmap for release 0.87 ========================
DATE : mars 2016
Release Notes (details in file CHANGES):
== TODO ==
* DONE finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
C'est finalisé. Mais les tuples restent polymorphes.
* DONE Coq realization of bitvector theory
* DONE support for both isabelle 2014 and 2015
+ bugfix for installation
* DONE review support for division operators by SMT provers
......
doc/macros.tex
View file @ 6bb5875d
......@@ -42,8 +42,12 @@
%%% listings for Why3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\RequirePackage{listings}
\RequirePackage{amssymb}
% cannot use \usepackage here because it breaks hevea (no colored keywords anymore :-()
\input{../share/latex/why3lang.sty}
% \RequirePackage{listings}
% \RequirePackage{amssymb}
\lstset{
basicstyle={\ttfamily},
......@@ -54,41 +58,9 @@
commentstyle=\itshape,
columns=[l]fullflexible,
showstringspaces=false,
literate=%
}
\lstdefinelanguage{why3}
{
morekeywords={namespace,predicate,function,inductive,type,use,clone,%
import,export,theory,module,end,in,with,%
let,rec,for,to,do,done,match,if,then,else,while,try,invariant,variant,%
absurd,raise,assert,exception,private,abstract,mutable,ghost,%
downto,raises,writes,reads,requires,ensures,returns,val,model,%
goal,axiom,lemma,forall,meta},%
string=[b]",%
sensitive=true,%
morecomment=[s]{(*}{*)},%
keepspaces=true,
}
%literate=%
%{'a}{$\alpha$}{1}%
%{'b}{$\beta$}{1}%
%{<}{$<$}{1}%
%{>}{$>$}{1}%
%{<=}{$\le$}{1}%
%{>=}{$\ge$}{1}%
% {<>}{$\ne$}{1}%
% {/\\}{$\land$}{1}%
% {\\/}{ $\lor$ }{3}%
% {\ or(}{ $\lor$(}{3}%
% {not\ }{$\lnot$ }{1}%
% {not(}{$\lnot$(}{1}%
% {+->}{\texttt{+->}}{2}%
% % {+->}{$\mapsto$}{2}%
% {-->}{\texttt{-\relax->}}{2}%
% %{-->}{$\longrightarrow$}{2}%
% {->}{$\rightarrow$}{2}%
% {<->}{$\leftrightarrow$}{2}%
\lstnewenvironment{whycode}{\lstset{language=why3}}{}
\lstnewenvironment{ocamlcode}{\lstset{language={[Objective]Caml}}}{}
......
doc/manpages.tex
View file @ 6bb5875d
......@@ -307,17 +307,36 @@ proof obligations, the corresponding proof attempts are marked obsolete.
actions are performed even if the goal is already proved. The second
choice allows to compare provers on the same goal.
\item[Strategies] section provides a set of actions that are
performed on the selected goal(s):
\begin{description}
\item[Split] splits the current goal into subgoals if it is a
conjunction of two or more goals. It corresponds to the
\verb|split_goal_wp| transformation.
\item[Inline] inlines the definitions in the conclusion of the goal.
It corresponds to the \verb|introduce_premises| transformation
follwoed by \verb|inline_goal|.
\item[Auto level 1] is a strategy that first applies a few provers
on the goal with a short time limit, then splits the goal and
tries again on the subgoals
\item[Auto level 2] is a strategy more elaborate than level 1, that
attempts to apply a few transformations that are typically
useful. It also tries the provers with a larger time limit.
\end{description}
A more detailed description of strategies is given in
Section~\ref{sec:strategies}, as well as a description on how to
design strategies of your own.
\item[Provers] provide a button for each detected prover. Clicking on such a
button starts the corresponding prover on the selected goal(s).
\item[Split] splits the current goal into subgoals if it is a
conjunction of two or more goals. It corresponds to the
\verb|split_goal_wp| transformation.
\item[Inline] replaces the head predicate symbol of the goal with its
definition. It corresponds to the
\verb|inline_goal| transformation.
% \item[Inline] replaces the head predicate symbol of the goal with its
% definition. It corresponds to the
% \verb|inline_goal| transformation.
\item[Tools] section provides a set of specific action that are
typically performed on the selected goal(s). :
\begin{description}
\item[Edit] starts an editor on the selected task.
For automatic provers, this allows to see the file sent to the
......@@ -340,6 +359,7 @@ proof obligations, the corresponding proof attempts are marked obsolete.
\item[Interrupt] cancels all the proof attempts currently scheduled
but not yet started.
\end{description}
\end{description}
......@@ -350,7 +370,7 @@ proof obligations, the corresponding proof attempts are marked obsolete.
\begin{description}
\item[Add File] adds a file in the GUI.
%\item[Detect provers] runs provers auto-detection
\item[Preferences] opens a window for modifying preferred
]\item[Preferences] opens a window for modifying preferred
configuration parameters, see details below.
\item[Reload] reloads the input files from disk, and update the session state accordingly.
\item[Save session] saves current session state on disk. The policy to decide when to save the session is configurable, as described in the preferences below.
......
doc/technical.tex
View file @ 6bb5875d
......@@ -604,6 +604,94 @@ and is likely to change in future versions.
\end{description}
\section{Proof Strategies}
\label{sec:strategies}
As seen in Section~\ref{sec:ideref}, the IDE provides a few buttons
that trigger the run of simple proof strategies on the selected goals.
Proof strategies can be defined using a basic assembly-style language,
and put into the Why3 configuration file. The commands of this basic
language are:
\begin{itemize}
\item \texttt{c $p$ $t$ $m$} calls the prover $p$ with a time limit
$t$ and memory limit $m$. On success, the strategy ends, it
continues to next line otherwise
\item \texttt{t $n$ $lab$} applies the transformation $n$. On success,
the strategy continues to label $lab$, and is applied to each
generated sub-goals. It continues to next line otherwise.
\item \texttt{g $lab$} inconditionally jumps to label $lab$
\item \texttt{$lab$:} declares the label $lab$. The default label
\texttt{exit} allows to stop the program.
\end{itemize}
To examplify this basic programming language, we give below the
default strategies that are attached to the default buttons of the
IDE, assuming that the provers Alt-Ergo 1.01, CVC4 1.4 and Z3 4.4.1
were detected by the \verb|why3 config --detect| command
\begin{description}
\item[Split] is bound to the 1-line strategy
\begin{verbatim}
t split_goal_wp exit
\end{verbatim}
\item[Auto level 1] is bound to
\begin{verbatim}
start:
c Z3,4.4.1, 1 1000
c Alt-Ergo,1.01, 1 1000
c CVC4,1.4, 1 1000
t split_goal_wp start
c Z3,4.4.1, 10 4000
c Alt-Ergo,1.01, 10 4000
c CVC4,1.4, 10 4000
\end{verbatim}
The three provers are first tried for a time limit of 1 second and
memory limit of 1~Gb, each in turn. If none of them succeed, a
split is attempted. If the split works then the same strategy is
retried on each sub-goals. If the split does not succeed, the provers
are tried again with a larger limits.
\item[Auto level 2] is bound to
\begin{verbatim}
start:
c Z3,4.4.1, 1 1000
c Eprover,1.8-001, 1 1000
c Spass,3.7, 1 1000
c Alt-Ergo,1.01, 1 1000
c CVC4,1.4, 1 1000
t split_goal_wp start
c Z3,4.4.1, 5 2000
c Eprover,1.8-001, 5 2000
c Spass,3.7, 5 2000
c Alt-Ergo,1.01, 5 2000
c CVC4,1.4, 5 2000
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
g trylongertime
afterinline:
t split_goal_wp start
trylongertime:
c Z3,4.4.1, 30 4000
c Eprover,1.8-001, 30 4000
c Spass,3.7, 30 4000
c Alt-Ergo,1.01, 30 4000
c CVC4,1.4, 30 4000
\end{verbatim}
Notice that now 5 provers are used. The provers are first tried for
a time limit of 1 second and memory limit of 1~Gb, each in turn. If
none of them succeed, a split is attempted. If the split works then
the same strategy is retried on each sub-goals. If the split does
not succeed, the prover are tried again with limits of 5 s and 2
Gb. If all fail, we attempt the transformation of introduction of
premises in the context, followed by an inlining of the definiiions
in the goals. We then attempt a split again, if the split succeeds,
we restart from the beginning, if it fails then provers are tried
again with 30s and 4 Gb.
\end{description}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
......
examples/avl/association_list/why3session.xml
View file @ 6bb5875d
......@@ -2,70 +2,69 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../association_list.mlw" expanded="true">
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../association_list.mlw">
<theory name="Assoc" sum="12adb5d5e7c156493bafb1bd121c4586">
<goal name="appear_append">
<proof prover="4"><result status="valid" time="0.03" steps="67"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="48"/></proof>
</goal>
<goal name="WP_parameter model_domain" expl="VC for model_domain">
<proof prover="4"><result status="valid" time="0.07" steps="233"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="274"/></proof>
</goal>
<goal name="WP_parameter model_key" expl="VC for model_key">
<proof prover="4"><result status="valid" time="0.04" steps="124"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="103"/></proof>
</goal>
<goal name="WP_parameter model_congruence" expl="VC for model_congruence">
<transf name="split_goal_wp">
<goal name="WP_parameter model_congruence.1" expl="1. variant decrease">
<proof prover="4"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter model_congruence.2" expl="2. precondition">
<proof prover="4"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter model_congruence.3" expl="3. postcondition">
<proof prover="4"><result status="valid" time="0.08" steps="194"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="127"/></proof>
</goal>
<goal name="WP_parameter model_congruence.4" expl="4. postcondition">
<proof prover="4"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter model_unique" expl="VC for model_unique">
<proof prover="4"><result status="valid" time="0.03" steps="160"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="108"/></proof>
</goal>
<goal name="WP_parameter model_singleton" expl="VC for model_singleton">
<proof prover="4"><result status="valid" time="0.02" steps="41"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="70"/></proof>
</goal>
<goal name="WP_parameter model_concat" expl="VC for model_concat">
<transf name="split_goal_wp">
<goal name="WP_parameter model_concat.1" expl="1. postcondition">
<proof prover="4"><result status="valid" time="0.03" steps="70"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="WP_parameter model_concat.2" expl="2. postcondition">
<proof prover="4"><result status="valid" time="0.03" steps="75"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="WP_parameter model_concat.3" expl="3. postcondition">
<proof prover="4"><result status="valid" time="0.03" steps="39"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="23"/></proof>
</goal>
<goal name="WP_parameter model_concat.4" expl="4. postcondition">
<proof prover="4"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter model_concat.5" expl="5. variant decrease">
<proof prover="4"><result status="valid" time="0.02" steps="29"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter model_concat.6" expl="6. precondition">
<proof prover="4"><result status="valid" time="0.02" steps="55"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="WP_parameter model_concat.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.45"/></proof>
<proof prover="1"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="WP_parameter model_concat.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter model_concat.9" expl="9. postcondition">
<proof prover="4"><result status="valid" time="0.09" steps="115"/></proof>
<proof prover="4"><result status="valid" time="0.09" steps="143"/></proof>
</goal>
<goal name="WP_parameter model_concat.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......@@ -73,26 +72,26 @@
</transf>
</goal>
</theory>
<theory name="AssocSorted" sum="c234d7458c225ff847c0ef368a2e5830" expanded="true">
<goal name="Eq.Refl" expanded="true">
<theory name="AssocSorted" sum="c234d7458c225ff847c0ef368a2e5830">
<goal name="Eq.Refl">
<proof prover="4"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="Eq.Trans" expanded="true">
<goal name="Eq.Trans">
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="Eq.Symm" expanded="true">
<goal name="Eq.Symm">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="S.O.Trans" expanded="true">
<goal name="S.O.Trans">
<proof prover="4"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter increasing_unique" expl="VC for increasing_unique">
<proof prover="4"><result status="valid" time="0.07" steps="85"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="66"/></proof>
</goal>
<goal name="WP_parameter model_cut" expl="VC for model_cut">
<transf name="split_goal_wp">
<goal name="WP_parameter model_cut.1" expl="1. assertion">
<proof prover="4"><result status="valid" time="0.04" steps="63"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="66"/></proof>
</goal>
<goal name="WP_parameter model_cut.2" expl="2. assertion">
<transf name="split_goal_wp">
......@@ -100,16 +99,16 @@
<proof prover="4"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.2" expl="2. assertion">
<proof prover="4"><result status="valid" time="0.08" steps="125"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="106"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.3" expl="3. assertion">
<proof prover="4"><result status="valid" time="0.02" steps="123"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="106"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.4" expl="4. assertion">
<proof prover="4"><result status="valid" time="0.02" steps="0"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.5" expl="5. assertion">
<proof prover="4"><result status="valid" time="0.03" steps="41"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="32"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.6" expl="6. assertion">
<proof prover="4"><result status="valid" time="0.08" steps="0"/></proof>
......@@ -122,10 +121,10 @@
<proof prover="4"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.2" expl="2. assertion">
<proof prover="4"><result status="valid" time="0.08" steps="122"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="104"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.3" expl="3. assertion">
<proof prover="4"><result status="valid" time="0.02" steps="152"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="136"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.4" expl="4. assertion">
<proof prover="4"><result status="valid" time="0.02" steps="0"/></proof>
......@@ -158,18 +157,18 @@
<proof prover="4"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="WP_parameter model_cut.7" expl="7. postcondition">
<proof prover="4"><result status="valid" time="0.13" steps="136"/></proof>
<proof prover="4"><result status="valid" time="0.13" steps="145"/></proof>
</goal>
<goal name="WP_parameter model_cut.8" expl="8. postcondition">
<proof prover="4"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="WP_parameter model_cut.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="4" steplimit="0"><result status="valid" time="0.11" steps="312"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter model_split" expl="VC for model_split">
<proof prover="0"><result status="valid" time="1.89"/></proof>
<proof prover="4" steplimit="0"><result status="valid" time="0.15" steps="686"/></proof>
</goal>
</theory>
</file>
......
examples/avl/avl/why3session.xml
View file @ 6bb5875d
......@@ -2,214 +2,420 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="2" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.3" timelimit="2" memlimit="0"/>
<file name="../avl.mlw" expanded="true">
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="2" steplimit="1" memlimit="0"/>
<file name="../avl.mlw">
<theory name="SelectionTypes" sum="8ee3f641805a143e052f3881ea88fc8c">
<goal name="rebuild_aternative_def">
<proof prover="1" memlimit="0"><result status="valid" time="0.07" steps="116"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.07" steps="88"/></proof>
</goal>
</theory>
<theory name="AVL" sum="ac42cb4292620577cf8c25d25a816879" expanded="true">
<theory name="AVL" sum="14e0e79e1c62330bf7a8042003faef03">
<goal name="M.M.assoc">
<proof prover="1" timelimit="5"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="1" steplimit="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="M.M.neutral">
<proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="1" steplimit="1"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter real_height_nonnegative" expl="VC for real_height_nonnegative">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="50"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="rotation_preserve_model">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="14"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter height" expl="VC for height">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="29"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter total" expl="VC for total">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="31"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter node" expl="VC for node">
<proof prover="1" memlimit="0"><result status="valid" time="0.16" steps="98"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.03" steps="98"/></proof>
</goal>
<goal name="WP_parameter singleton" expl="VC for singleton">
<proof prover="1" memlimit="0"><result status="valid" time="0.04" steps="87"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.04" steps="63"/></proof>
</goal>
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="1" memlimit="0"><result status="valid" time="0.13" steps="78"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.13" steps="68"/></proof>
</goal>
<goal name="WP_parameter view" expl="VC for view">
<proof prover="1" memlimit="0"><result status="valid" time="0.07" steps="241"/></proof>
<proof prover="1" timelimit="2" steplimit="1" memlimit="0"><result status="valid" time="0.07" steps="257"/></proof>
</goal>
<goal name="WP_parameter balance" expl="VC for balance">
<transf name="split_goal_wp">
<goal name="WP_parameter balance.1" expl="1. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter balance.2" expl="2. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter balance.3" expl="3. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter balance.4" expl="4. unreachable point">
<proof prover="1" memlimit="0"><result status="valid" time="0.04" steps="55"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="WP_parameter balance.5" expl="5. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.05" steps="62"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="WP_parameter balance.6" expl="6. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.06" steps="72"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="WP_parameter balance.7" expl="7. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="96"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="83"/></proof>
</goal>
<goal name="WP_parameter balance.8" expl="8. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.19" steps="162"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="125"/></proof>
</goal>
<goal name="WP_parameter balance.9" expl="9. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.33" steps="283"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="63"/></proof>
</goal>
<goal name="WP_parameter balance.10" expl="10. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.33" steps="292"/></proof>
<proof prover="1"><result status="valid" time="0.14" steps="209"/></proof>
</goal>
<goal name="WP_parameter balance.11" expl="11. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter balance.12" expl="12. unreachable point">