diff --git a/.gitignore b/.gitignore index 1819c8542a116e7c7fd5b1fec6bc41343f8728b8..ab6eb01adda1bc296b3e256ddff021dc8e8cf951 100644 --- a/.gitignore +++ b/.gitignore @@ -120,21 +120,17 @@ why3.conf /doc/manual.synctex.gz /doc/*.haux /doc/*.pdf +/doc/generated/ /doc/html/ /doc/*.hind /doc/*.htoc /doc/bnf /doc/bnf.ml -/doc/*_bnf.tex /doc/apidoc.tex /doc/apidoc/ /doc/stdlibdoc/ /doc/texput.log /doc/extract_ocaml_code -/doc/logic_*.ml -/doc/call_provers_*.ml -/doc/whyconf_*.ml -/doc/*__*.ml # /lib /lib/why3-cpulimit diff --git a/Makefile.in b/Makefile.in index cab9aaef027c55fffd840e8c5457361118fe1005..e38dd4eb4e80e36c9bed3617ded5c4cc54657991 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1860,9 +1860,9 @@ doc: doc/manual.pdf doc/html/index.html BNF = ident qualid attribute constant operator type formula term1 term2 term3 \ theory theory2 \ why_file spec expr expr2 module whyml_file term_old_at -BNFTEX = $(BNF:%=doc/%_bnf.tex) +BNFTEX = $(BNF:%=doc/generated/%_bnf.tex) -doc/%_bnf.tex: doc/%.bnf doc/bnf$(EXE) +doc/generated/%_bnf.tex: doc/%.bnf doc/bnf$(EXE) doc/bnf$(EXE) $< > $@ doc/bnf$(EXE): doc/bnf.mll @@ -1872,19 +1872,19 @@ doc/bnf$(EXE): doc/bnf.mll doc/extract_ocaml_code: doc/extract_ocaml_code.ml $(OCAMLC) str.cma -o $@ $< -doc/logic__%.ml: examples/use_api/logic.ml doc/extract_ocaml_code +doc/generated/logic__%.ml: examples/use_api/logic.ml doc/extract_ocaml_code doc/extract_ocaml_code $* < $< > $@ -doc/whyconf__%.ml: src/driver/whyconf.ml doc/extract_ocaml_code +doc/generated/whyconf__%.ml: src/driver/whyconf.ml doc/extract_ocaml_code doc/extract_ocaml_code $* < $< > $@ -doc/call_provers__%.ml: src/driver/call_provers.ml doc/extract_ocaml_code +doc/generated/call_provers__%.ml: src/driver/call_provers.ml doc/extract_ocaml_code doc/extract_ocaml_code $* < $< > $@ -doc/mlw_tree__%.ml: examples/use_api/mlw_tree.ml doc/extract_ocaml_code +doc/generated/mlw_tree__%.ml: examples/use_api/mlw_tree.ml doc/extract_ocaml_code doc/extract_ocaml_code $* < $< > $@ -doc/transform__%.ml: examples/use_api/transform.ml doc/extract_ocaml_code +doc/generated/transform__%.ml: examples/use_api/transform.ml doc/extract_ocaml_code doc/extract_ocaml_code $* < $< > $@ OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \ @@ -1904,11 +1904,12 @@ OCAMLCODE_MLWTREE = buildenv openmodule useimport \ source1 code1 helper1 source2 code2 source3 code3 \ closemodule checkingvcs -OCAMLCODE = $(addprefix doc/logic__, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \ - $(addprefix doc/call_provers__, $(addsuffix .ml, $(OCAMLCODE_CALLPROVERS))) \ - $(addprefix doc/transform__, $(addsuffix .ml, $(OCAMLCODE_TRANSFORM))) \ - $(addprefix doc/mlw_tree__, $(addsuffix .ml, $(OCAMLCODE_MLWTREE))) \ - doc/whyconf__provertype.ml +OCAMLCODE = \ + $(addprefix doc/generated/logic__, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \ + $(addprefix doc/generated/call_provers__, $(addsuffix .ml, $(OCAMLCODE_CALLPROVERS))) \ + $(addprefix doc/generated/transform__, $(addsuffix .ml, $(OCAMLCODE_TRANSFORM))) \ + $(addprefix doc/generated/mlw_tree__, $(addsuffix .ml, $(OCAMLCODE_MLWTREE))) \ + doc/generated/whyconf__provertype.ml DOC = api glossary ide intro exec macros manpages install \ manual starting syntax syntaxref technical version whyml \ diff --git a/doc/api.tex b/doc/api.tex index 9dbfa00c2bfacdb88e6fcdcf7ee58b37f01701a4..4c1db1226c0fda259bc3d0e2d363dbc1fdbcfd3a 100644 --- a/doc/api.tex +++ b/doc/api.tex @@ -24,7 +24,7 @@ The first step is to know how to build propositional formulas. The module \texttt{Term} gives a few functions for building these. Here is a piece of OCaml code for building the formula $\mathit{true} \lor \mathit{false}$. -\lstinputlisting{logic__opening.ml} +\lstinputlisting{generated/logic__opening.ml} The library uses the common type \texttt{term} both for terms (\ie expressions that produce a value of some particular type) and formulas (\ie boolean-valued expressions). @@ -35,7 +35,7 @@ and formulas (\ie boolean-valued expressions). Such a formula can be printed using the module \texttt{Pretty} providing pretty-printers. -\lstinputlisting{logic__printformula.ml} +\lstinputlisting{generated/logic__printformula.ml} Assuming the lines above are written in a file \texttt{f.ml}, it can be compiled using @@ -50,12 +50,12 @@ formula 1 is: true \/ false Let us now build a formula with propositional variables: $A \land B \rightarrow A$. Propositional variables must be declared first before using them in formulas. This is done as follows. -\lstinputlisting{logic__declarepropvars.ml} +\lstinputlisting{generated/logic__declarepropvars.ml} The type \texttt{lsymbol} is the type of function and predicate symbols (which we call logic symbols for brevity). Then the atoms $A$ and $B$ must be built by the general function for applying a predicate symbol to a list of terms. Here we just need the empty list of arguments. -\lstinputlisting{logic__declarepropatoms.ml} +\lstinputlisting{generated/logic__declarepropatoms.ml} As expected, the output is as follows. \begin{verbatim} @@ -74,7 +74,7 @@ tasks from our formulas. Task can be build incrementally from an empty task by adding declaration to it, using the functions \texttt{add\_*\_decl} of module \texttt{Task}. For the formula $\mathit{true} \lor \mathit{false}$ above, this is done as follows. -\lstinputlisting{logic__buildtask.ml} +\lstinputlisting{generated/logic__buildtask.ml} To make the formula a goal, we must give a name to it, here ``goal1''. A goal name has type \texttt{prsymbol}, for identifiers denoting propositions in a theory or a task. Notice again that the concrete @@ -86,12 +86,12 @@ Notice that lemmas are not allowed in tasks and can only be used in theories. Once a task is built, it can be printed. -\lstinputlisting{logic__printtask.ml} +\lstinputlisting{generated/logic__printtask.ml} The task for our second formula is a bit more complex to build, because the variables A and B must be added as abstract (\ie not defined) propositional symbols in the task. -\lstinputlisting{logic__buildtask2.ml} +\lstinputlisting{generated/logic__buildtask2.ml} Execution of our OCaml program now outputs: \begin{verbatim} @@ -118,44 +118,44 @@ file \texttt{why3.conf}, as it was built using the \texttt{why3config} command line tool or the \textsf{Detect Provers} menu of the graphical IDE. The following API calls allow to access the content of this configuration file. -\lstinputlisting{logic__getconf.ml} +\lstinputlisting{generated/logic__getconf.ml} The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A prover is a record with a name, a version, and an alternative description (to differentiate between various configurations of a given prover). Its definition is in the module \texttt{Whyconf}: -\lstinputlisting{whyconf__provertype.ml} +\lstinputlisting{generated/whyconf__provertype.ml} The map \texttt{provers} provides the set of existing provers. In the following, we directly attempt to access a prover named ``Alt-Ergo'', any version. -\lstinputlisting{logic__getanyaltergo.ml} +\lstinputlisting{generated/logic__getanyaltergo.ml} We could also get a specific version with : -\lstinputlisting{logic__getaltergo200.ml} +\lstinputlisting{generated/logic__getaltergo200.ml} The next step is to obtain the driver associated to this prover. A driver typically depends on the standard theories so these should be loaded first. -\lstinputlisting{logic__getdriver.ml} +\lstinputlisting{generated/logic__getdriver.ml} We are now ready to call the prover on the tasks. This is done by a function call that launches the external executable and waits for its termination. Here is a simple way to proceed: -\lstinputlisting{logic__callprover.ml} +\lstinputlisting{generated/logic__callprover.ml} This way to call a prover is in general too naive, since it may never return if the prover runs without time limit. The function \texttt{prove\_task} has an optional parameter \texttt{limit}, a record defined in module \texttt{Call\_provers}: -\lstinputlisting{call_provers__resourcelimit.ml} +\lstinputlisting{generated/call_provers__resourcelimit.ml} where the field \texttt{limit\_time} is the maximum allowed running time in seconds, and \texttt{limit\_mem} is the maximum allowed memory in megabytes. The type \texttt{prover\_result} is a record defined in module \texttt{Call\_provers}: -\lstinputlisting{call_provers__proverresult.ml} +\lstinputlisting{generated/call_provers__proverresult.ml} with in particular the fields: \begin{itemize} \item \texttt{pr\_answer}: the prover answer, explained below; \item \texttt{pr\_time} : the time taken by the prover, in seconds. \end{itemize} A \texttt{pr\_answer} is the sum type defined in module \texttt{Call\_provers}: -\lstinputlisting{call_provers__proveranswer.ml} +\lstinputlisting{generated/call_provers__proveranswer.ml} corresponding to these kinds of answers: \begin{itemize} \item \texttt{Valid}: the task is valid according to the prover. @@ -174,7 +174,7 @@ corresponding to these kinds of answers: \end{itemize} Here is thus another way of calling the Alt-Ergo prover, on our second task. -\lstinputlisting{logic__calltimelimit.ml} +\lstinputlisting{generated/logic__calltimelimit.ml} The output of our program is now as follows. \begin{verbatim} On task 1, alt-ergo answers Valid (0.01s) @@ -191,29 +191,29 @@ Here is the way we build the formula $2+2=4$. The main difficulty is to access the internal identifier for addition: it must be retrieved from the standard theory \texttt{Int} of the file \texttt{int.why} (see Chap~\ref{sec:library}). -\lstinputlisting{logic__buildfmla.ml} +\lstinputlisting{generated/logic__buildfmla.ml} An important point to notice as that when building the application of $+$ to the arguments, it is checked that the types are correct. Indeed the constructor \texttt{t\_app\_infer} infers the type of the resulting term. One could also provide the expected type as follows. -\lstinputlisting{logic__buildtermalt.ml} +\lstinputlisting{generated/logic__buildtermalt.ml} When building a task with this formula, we need to declare that we use theory \texttt{Int}: -\lstinputlisting{logic__buildtaskimport.ml} +\lstinputlisting{generated/logic__buildtaskimport.ml} \section{Building Quantified Formulas} To illustrate how to build quantified formulas, let us consider the formula $\forall x:int. x*x \geq 0$. The first step is to obtain the symbols from \texttt{Int}. -\lstinputlisting{logic__quantfmla1.ml} +\lstinputlisting{generated/logic__quantfmla1.ml} The next step is to introduce the variable $x$ with the type int. -\lstinputlisting{logic__quantfmla2.ml} +\lstinputlisting{generated/logic__quantfmla2.ml} The formula $x*x \geq 0$ is obtained as in the previous example. -\lstinputlisting{logic__quantfmla3.ml} +\lstinputlisting{generated/logic__quantfmla3.ml} To quantify on $x$, we use the appropriate smart constructor as follows. -\lstinputlisting{logic__quantfmla4.ml} +\lstinputlisting{generated/logic__quantfmla4.ml} \section{Building Theories} @@ -226,33 +226,33 @@ be done by a sequence of calls: \end{itemize} Creation of a theory named \verb|My_theory| is done by -\lstinputlisting{logic__buildth1.ml} +\lstinputlisting{generated/logic__buildth1.ml} First let us add formula 1 above as a goal: -\lstinputlisting{logic__buildth2.ml} +\lstinputlisting{generated/logic__buildth2.ml} Note that we reused the goal identifier \verb|goal_id1| that we already defined to create task 1 above. Adding formula 2 needs to add the declarations of predicate variables A and B first: -\lstinputlisting{logic__buildth3.ml} +\lstinputlisting{generated/logic__buildth3.ml} Adding formula 3 is a bit more complex since it uses integers, thus it requires to ``use'' the theory \verb|int.Int|. Using a theory is indeed not a primitive operation in the API: it must be done by a combination of an ``export'' and the creation of a namespace. We provide a helper function for that: -\lstinputlisting{logic__buildth4.ml} +\lstinputlisting{generated/logic__buildth4.ml} Addition of formula 3 is then -\lstinputlisting{logic__buildth5.ml} +\lstinputlisting{generated/logic__buildth5.ml} Addition of goal 4 is nothing more complex: -\lstinputlisting{logic__buildth6.ml} +\lstinputlisting{generated/logic__buildth6.ml} Finally, we close our theory under construction as follows. -\lstinputlisting{logic__buildth7.ml} +\lstinputlisting{generated/logic__buildth7.ml} We can inspect what we did by printing that theory: -\lstinputlisting{logic__printtheory.ml} +\lstinputlisting{generated/logic__printtheory.ml} which outputs \begin{verbatim} my new theory is as follows: @@ -278,12 +278,12 @@ end From a theory, one can compute at once all the proof tasks it contains as follows: -\lstinputlisting{logic__splittheory.ml} +\lstinputlisting{generated/logic__splittheory.ml} Note that the tasks are returned in reverse order, so we reverse the list above. We can check our generated tasks by printing them: -\lstinputlisting{logic__printalltasks.ml} +\lstinputlisting{generated/logic__printalltasks.ml} One can run provers on those tasks exactly as we did above. @@ -293,12 +293,12 @@ The following code illustrates a simple recursive functions of formulas. It explores the formula and when a negation is found, it tries to push it down below a conjunction, a disjunction or a quantifier. -\lstinputlisting{transform__negate.ml} +\lstinputlisting{generated/transform__negate.ml} The following illustrates how to turn such an OCaml function into a transformation in the sens of Why3 API. moreover, it registers that transformation to make it available for example in Why3 IDE. -\lstinputlisting{transform__register.ml} +\lstinputlisting{generated/transform__register.ml} The directory \verb|src/transform| contains the code for the many transformations that are already available in Why3. @@ -322,13 +322,13 @@ The first step is to build an environment as already illustrated in Section~\ref{sec:api:callingprovers}, and open the OCaml module \verb|Ptree| which contains most of the OCaml functions we need in this section. -\lstinputlisting{mlw_tree__buildenv.ml} +\lstinputlisting{generated/mlw_tree__buildenv.ml} To contain all the example programs we are going to build we need a module. We start the creation of that module using the following declarations, that first introduces a pseudo ``file'' to hold the module, then the module itself called \verb|Program|. -\lstinputlisting{mlw_tree__openmodule.ml} +\lstinputlisting{generated/mlw_tree__openmodule.ml} Notice the use of a first simple helper function \verb|mk_ident| to build an identifier without any label nor any location. @@ -337,39 +337,39 @@ To write our programs, we need to import some other modules from the standard library. The following introduces two helper functions for building qualified identifiers and importing modules, and finally imports \verb|int.Int|. -\lstinputlisting{mlw_tree__useimport.ml} +\lstinputlisting{generated/mlw_tree__useimport.ml} We want now to build a program equivalent to the following code in concrete Why3 syntax. -\lstinputlisting[language=why3]{mlw_tree__source1.ml} +\lstinputlisting[language=why3]{generated/mlw_tree__source1.ml} The OCaml code that programmatically build this Why3 function is as follows. -\lstinputlisting{mlw_tree__code1.ml} +\lstinputlisting{generated/mlw_tree__code1.ml} This code makes uses of helper functions that are given in Figure~\ref{fig:helpers}. \begin{figure}[t] - \lstinputlisting{mlw_tree__helper1.ml} + \lstinputlisting{generated/mlw_tree__helper1.ml} \caption{Helper functions for building WhyML programs} \label{fig:helpers} \end{figure} We want now to build a program equivalent to the following code in concrete Why3 syntax. -\lstinputlisting[language=why3]{mlw_tree__source2.ml} +\lstinputlisting[language=why3]{generated/mlw_tree__source2.ml} We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows -\lstinputlisting{mlw_tree__code2.ml} +\lstinputlisting{generated/mlw_tree__code2.ml} The next example makes use of arrays. -\lstinputlisting[language=why3]{mlw_tree__source3.ml} +\lstinputlisting[language=why3]{generated/mlw_tree__source3.ml} The corresponding OCaml code is as follows -\lstinputlisting{mlw_tree__code3.ml} +\lstinputlisting{generated/mlw_tree__code3.ml} Having declared all the programs we wanted to write, we can now close the module and the file, and get as a result the set of modules of our file, under the form of a map of module names to modules. -\lstinputlisting{mlw_tree__closemodule.ml} +\lstinputlisting{generated/mlw_tree__closemodule.ml} We can then construct the proofs tasks for our module, and then try to call the Alt-Ergo prover. The reste of that code is using OCaml functions that were already introduced before. -\lstinputlisting{mlw_tree__checkingvcs.ml} +\lstinputlisting{generated/mlw_tree__checkingvcs.ml} %%% Local Variables: %%% mode: latex diff --git a/doc/generated/.keepme b/doc/generated/.keepme new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/doc/language.tex b/doc/language.tex index 3def7bef26c46ce6a1d663abf43887da91c444a5..454707663dbbd4a6da0872e763aa1f8fcd969380 100644 --- a/doc/language.tex +++ b/doc/language.tex @@ -178,7 +178,7 @@ In the following, strings are referred to with the non-terminal uppercase identifiers and, similarly, lowercase and uppercase qualified identifiers. -\begin{center}\framebox{\input{./qualid_bnf.tex}}\end{center} +\begin{center}\framebox{\input{./generated/qualid_bnf.tex}}\end{center} \paragraph{Constants.} The syntax for constants is given in Figure~\ref{fig:bnf:constant}. @@ -187,7 +187,7 @@ Integer constants may be given in base 16, 10, 8 or 2. Real constants may be given in base 16 or 10. \begin{figure} -\begin{center}\framebox{\input{./constant_bnf.tex}}\end{center} +\begin{center}\framebox{\input{./generated/constant_bnf.tex}}\end{center} \caption{Syntax for constants.} \label{fig:bnf:constant} \end{figure} @@ -195,7 +195,7 @@ Real constants may be given in base 16 or 10. \paragraph{Operators.} Prefix and infix operators are built from characters organized in four categories (\textsl{op-char-1} to \textsl{op-char-4}). -\begin{center}\framebox{\input{./operator_bnf.tex}}\end{center} +\begin{center}\framebox{\input{./generated/operator_bnf.tex}}\end{center} Infix operators are classified into 4 categories, according to the characters they are built from: \begin{itemize} @@ -211,7 +211,7 @@ characters they are built from: \paragraph{Labels.} Identifiers, terms, formulas, program expressions can all be labeled, either with a string, or with a location tag. -\begin{center}\framebox{\input{./label_bnf.tex}}\end{center} +\begin{center}\framebox{\input{./generated/label_bnf.tex}}\end{center} A location tag consists of a file name, a line number, and starting and ending characters. diff --git a/doc/syntaxref.tex b/doc/syntaxref.tex index cf265c3dd5aa0bcfdb4e3f9faf9e1f00b2e06c4e..19af19ebc4db391ed1e528092e3e54d70f9088d0 100644 --- a/doc/syntaxref.tex +++ b/doc/syntaxref.tex @@ -25,7 +25,7 @@ In the following, strings are referred to with the non-terminal %\subsection{Constants} The syntax for numerical constants is given by the following rules: %\begin{figure}[ht] -\begin{center}\input{./constant_bnf.tex}\end{center} +\begin{center}\input{./generated/constant_bnf.tex}\end{center} %\caption{Syntax for numerical constants.} %\label{fig:bnf:constant} %\end{figure} @@ -42,7 +42,7 @@ The syntax distinguishes identifiers that start with a lowercase letter or an underscore (\nonterm{lident}{}\spacefalse) and identifiers that start with an uppercase letter (\nonterm{uident}{}\spacefalse): %\begin{figure}[ht] -\begin{center}\input{./ident_bnf.tex}\end{center} +\begin{center}\input{./generated/ident_bnf.tex}\end{center} %\caption{Syntax for identifiers.} %\label{fig:bnf:ident} %\end{figure} @@ -56,7 +56,7 @@ Prefix and infix operators are built from characters organized in four precedence groups (\textsl{op-char-1} to \textsl{op-char-4}): %as shown in Figure~\ref{fig:bnf:operator}. %\begin{figure}[ht] -\begin{center}\input{./operator_bnf.tex}\end{center} +\begin{center}\input{./generated/operator_bnf.tex}\end{center} %\caption{Syntax for operators.} %\label{fig:bnf:operator} %\end{figure} @@ -80,7 +80,7 @@ are always recognized as bang operators. %Qualified identifiers are prefixed with a sequence of uppercase %identifiers, e.g., \texttt{App.S.get}: %\begin{figure}[ht] -%\begin{center}\input{./qualid_bnf.tex}\end{center} +%\begin{center}\input{./generated/qualid_bnf.tex}\end{center} %\caption{Syntax for qualified identifiers.} %\label{fig:bnf:qualid} %\end{figure} @@ -88,7 +88,7 @@ are always recognized as bang operators. Finally, any identifier, term, formula, or expression in a \whyml source can be tagged either with a string \textit{attribute} or a location: -\begin{center}\input{./attribute_bnf.tex}\end{center} +\begin{center}\input{./generated/attribute_bnf.tex}\end{center} An attribute cannot contain newlines or closing square brackets; leading and trailing spaces are ignored. A location consists of a file name in double quotes, @@ -100,7 +100,7 @@ a line number, and starting and ending character positions. \whyml features an ML-style type system with polymorphic types, variants (sum types), and records that can have mutable fields. The syntax for type expressions is the following: -\begin{center}\input{./type_bnf.tex}\end{center} +\begin{center}\input{./generated/type_bnf.tex}\end{center} Built-in types are \texttt{int} (arbitrary precision integers), \texttt{real} (real numbers), \texttt{bool}, the arrow type (also called the \textit{mapping type}, right-associative), @@ -144,19 +144,19 @@ syntactical level, and \why will perform the necessary conversions behind the scenes. \begin{figure}[ht] -\begin{center}\input{./term1_bnf.tex}\end{center} +\begin{center}\input{./generated/term1_bnf.tex}\end{center} \caption{\whyml terms (part I).} \label{fig:bnf:term1} \end{figure} \begin{figure}[ht] -\begin{center}\input{./term2_bnf.tex}\end{center} +\begin{center}\input{./generated/term2_bnf.tex}\end{center} \caption{\whyml terms (part II).} \label{fig:bnf:term2} \end{figure} \begin{figure}[ht] -\begin{center}\input{./term3_bnf.tex}\end{center} +\begin{center}\input{./generated/term3_bnf.tex}\end{center} \caption{\whyml terms (part III).} \label{fig:bnf:term3} \end{figure} @@ -281,7 +281,7 @@ Note that infix symbols of level 1 include equality (\texttt{=}) and disequality (\texttt{<>}). \begin{figure} - \begin{center}\framebox{\input{./formula_bnf.tex}}\end{center} + \begin{center}\framebox{\input{./generated/formula_bnf.tex}}\end{center} \caption{Syntax for formulas.} \label{fig:bnf:formula} \end{figure} @@ -305,13 +305,13 @@ transformations interpret those connectives as introduction of logical cuts The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bnf:theoryb}. \begin{figure} - \begin{center}\framebox{\input{./theory_bnf.tex}}\end{center} + \begin{center}\framebox{\input{./generated/theory_bnf.tex}}\end{center} \caption{Syntax for theories (part 1).} \label{fig:bnf:theorya} \end{figure} \begin{figure} - \begin{center}\framebox{\input{./theory2_bnf.tex}}\end{center} + \begin{center}\framebox{\input{./generated/theory2_bnf.tex}}\end{center} \caption{Syntax for theories (part 2).} \label{fig:bnf:theoryb} \end{figure} @@ -414,7 +414,7 @@ This type is used in the standard library in the theories \subsection{Files} A \why input file is a (possibly empty) list of theories. -\begin{center}\framebox{\input{./why_file_bnf.tex}}\end{center} +\begin{center}\framebox{\input{./generated/why_file_bnf.tex}}\end{center} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -426,13 +426,13 @@ A \why input file is a (possibly empty) list of theories. The syntax for specification clauses in programs is given in Figure~\ref{fig:bnf:spec}. \begin{figure} - \begin{center}\framebox{\input{./spec_bnf.tex}}\end{center} + \begin{center}\framebox{\input{./generated/spec_bnf.tex}}\end{center} \caption{Specification clauses in programs.} \label{fig:bnf:spec} \end{figure} Within specifications, terms are extended with new constructs \verb|old| and \verb|at|: -\begin{center}\framebox{\input{./term_old_at_bnf.tex}}\end{center} +\begin{center}\framebox{\input{./generated/term_old_at_bnf.tex}}\end{center} Within a postcondition, $\verb|old|~t$ refers to the value of term $t$ in the prestate. Within the scope of a code mark $L$, the term $\verb|at|~t~\verb|'|L$ refers to the value of term $t$ at the program @@ -443,13 +443,13 @@ point corresponding to $L$. The syntax for program expressions is given in Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}. \begin{figure} - \begin{center}\framebox{\input{./expr_bnf.tex}}\end{center} + \begin{center}\framebox{\input{./generated/expr_bnf.tex}}\end{center} \caption{Syntax for program expressions (part 1).} \label{fig:bnf:expra} \end{figure} \begin{figure} - \begin{center}\framebox{\input{./expr2_bnf.tex}}\end{center} + \begin{center}\framebox{\input{./generated/expr2_bnf.tex}}\end{center} \caption{Syntax for program expressions (part 2).} \label{fig:bnf:exprb} \end{figure} @@ -601,7 +601,7 @@ right, lazily. The syntax for modules is given in Figure~\ref{fig:bnf:module}. \begin{figure} - \begin{center}\framebox{\input{./module_bnf.tex}}\end{center} + \begin{center}\framebox{\input{./generated/module_bnf.tex}}\end{center} \caption{Syntax for modules.} \label{fig:bnf:module} \end{figure} @@ -613,7 +613,7 @@ variables, functions, exceptions). \subsection{Files} A \whyml input file is a (possibly empty) list of theories and modules. -\begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center} +\begin{center}\framebox{\input{./generated/whyml_file_bnf.tex}}\end{center} A theory defined in a \whyml file can only be used within that file. If a theory is supposed to be reused from other files, be they \why or \whyml files, it should be defined in a \why file.