Why3

https://why3.org/doc/
Admin
Why3 is a platform for deductive program verification providing the WhyML specification and...
Tokens:218,541
Snippets:1,775
Trust Score:7.5
Update:2 weeks ago
Show doc for...
Tokens:
Raw
### Test Why3 installation with examples

Source: https://why3.org/doc/_sources/install.rst.txt

Run example replays to verify the installation, expecting successful replay counts.

```console
$ cd examples
$ why3 replay logic/scottish-private-club
 1/1 (replay OK)
$ why3 replay same_fringe
 18/18 (replay OK)
```

--------------------------------

### Start Isabelle server and Why3 IDE

Source: https://why3.org/doc/_sources/itp.rst.txt

Start an Isabelle server and then launch Why3 IDE with the use_server wrapper to process proofs in the genealogy example.

```shell
isabelle server &
```

```shell
isabelle use_server why3 ide genealogy
```

--------------------------------

### Install Why3 with make install

Source: https://why3.org/doc/_sources/install.rst.txt

Install Why3, possibly as super-user.

```shell
make install
```

--------------------------------

### Test installation with why3 replay

Source: https://why3.org/doc/install.html

Run these commands to test the installation. The output shows expected results when required provers are installed.

```bash
$ cd examples
$ why3 replay logic/scottish-private-club
 1/1 (replay OK)
$ why3 replay same_fringe
 18/18 (replay OK)

```

--------------------------------

### Install Why3 from sources: configure, make, make install

Source: https://why3.org/doc/install.html

Run these commands in the why3-1.8 directory after unpacking the distribution. The configure script checks requirements; make compiles; make install installs (as super-user if needed).

```bash
./configure
make
make install

```

--------------------------------

### Configure, build, and install Why3 from source

Source: https://why3.org/doc/_sources/install.rst.txt

Standard sequence to compile and install Why3 from source.

```shell
./configure
make
make install
```

--------------------------------

### Install Why3

Source: https://why3.org/doc/install.html

Installs Why3, possibly as super-user if needed.

```bash
make install

```

--------------------------------

### Compile and install fixpoint library

Source: https://why3.org/doc/_sources/install.rst.txt

Compile and install the fixpoint library, a dependency of the infer-loop utility. The commands are an example and can be run in any directory. Modify Makefile.config if required before compiling.

```shell
svn co svn://scm.gforge.inria.fr/svnroot/bjeannet/pkg/fixpoint
cd fixpoint/trunk/
cp Makefile.config.model Makefile.config
# if required make modifications to Makefile.config
make all     # compiles
make install # uses ocamlfind to install the library
```

--------------------------------

### Install the Why3 API

Source: https://why3.org/doc/_sources/install.rst.txt

Install the Why3 API. Note that if your OCaml installation relies on Opam installed in your own user space, make install-lib should not be run as super-user.

```shell
make byte opt
make install-lib
```

--------------------------------

### Start Isabelle/jEdit server

Source: https://why3.org/doc/_sources/itp.rst.txt

Start the Isabelle/jEdit interface in server mode before launching why3 ide.

```shell
isabelle why3_jedit
```

--------------------------------

### Start Isabelle server

Source: https://why3.org/doc/itp.html

Start an Isabelle server in the background to speed up batch proof processing. Required before using isabelle use_server.

```bash
isabelle server &

```

--------------------------------

### InvertingAnInjection module setup and predicates

Source: https://why3.org/doc/_sources/whyml.rst.txt

Starts the InvertingAnInjection module by importing arithmetic and arrays, then defines logical predicates for injective, surjective, and range, and states the lemma that an injective array in range is also surjective.

```whyml
module InvertingAnInjection
  use int.Int
  use array.Array
```

```whyml
  predicate injective (a: array int) (n: int) =
    forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j]

  predicate surjective (a: array int) (n: int) =
    forall i. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i)
```

```whyml
  predicate range (a: array int) (n: int) =
    forall i. 0 <= i < n -> 0 <= a[i] < n
```

```whyml
  lemma injective_surjective:
    forall a: array int, n: int.
      injective a n -> range a n -> surjective a n
```

--------------------------------

### Install Why3 IDE via Opam

Source: https://why3.org/doc/_sources/install.rst.txt

Install the graphical user interface for Why3 using Opam.

```shell
opam install why3-ide
```

--------------------------------

### Install bash completion from Why3 sources

Source: https://why3.org/doc/_sources/install.rst.txt

Install the bash completion configuration for Why3 from the Why3 sources. Requires sudo privileges.

```shell
sudo make install-bash
```

--------------------------------

### Install bash completion directly

Source: https://why3.org/doc/install.html

Alternative command to install the bash completion file directly to /etc/bash_completion.d using the path from why3 --print-datadir.

```bash
sudo /usr/bin/install -c `why3 --print-datadir`/bash/why3 /etc/bash_completion.d

```

--------------------------------

### Install bash completion via make

Source: https://why3.org/doc/install.html

Run this command from the Why3 sources to install the bash completion configuration using make.

```bash
sudo make install-bash

```

--------------------------------

### Install Why3 via Opam

Source: https://why3.org/doc/_sources/install.rst.txt

Install the core Why3 package using the OCaml package manager.

```shell
opam install why3
```

--------------------------------

### Start NQueens module with imports

Source: https://why3.org/doc/_sources/whyml.rst.txt

Starts the N-Queens module by importing integer arithmetic and arrays from the standard library.

```whyml
module NQueens
  use int.Int
  use array.Array
```

--------------------------------

### Install bash completion directly

Source: https://why3.org/doc/_sources/install.rst.txt

Directly install the bash completion configuration for Why3 by copying the file from the shared data directory to /etc/bash_completion.d. Requires sudo privileges.

```shell
sudo /usr/bin/install -c `why3 --print-datadir`/bash/why3 /etc/bash_completion.d
```

--------------------------------

### why3 config add-prover example with Alt-Ergo

Source: https://why3.org/doc/manpages.html

Example that registers an Alt-Ergo executable at /home/me/bin/alt-ergo-trunk with shortcut new-ae. Manually added provers are stored in the configuration file under [partial_prover] sections with a field manual = true.

```bash
why3 config add-prover Alt-Ergo /home/me/bin/alt-ergo-trunk new-ae
```

--------------------------------

### why3 prove --sub-goal example

Source: https://why3.org/doc/_sources/manpages.rst.txt

Example command to prove only preconditions at line 123 in file.mlw using the --sub-goal option. The output shows the sub-goal explanation format.

```text
why3 prove --sub-goal=:123@Precondition file.mlw
```

```text
File "file.mlw", line 123, characters 0-1:
Sub-goal <expl> from goal f'vc.
```

--------------------------------

### Add Why3 Isabelle library path

Source: https://why3.org/doc/itp.html

Add this path to the Isabelle components file to make Why3's Isabelle setup available. Required after installing Why3.

```text
<Why3 lib dir>/isabelle

```

--------------------------------

### Compile OCaml file with Why3 library

Source: https://why3.org/doc/_sources/api.rst.txt

Compile an OCaml file that uses the Why3 library. Requires the Why3 library to be installed and the file f.ml to contain the code from the previous examples.

```shell
ocamlfind ocamlc -package why3 -linkpkg f.ml -o f
```

--------------------------------

### induction transform example: base and recursive cases

Source: https://why3.org/doc/_sources/technical.rst.txt

Applying induction n on the goal performs induction on n starting at 0. The base case adds axiom Init : n <= 0, while the recursive case adds Init : 0 < n and the induction hypothesis Hrec.

```whyml
constant n : int
predicate p int
predicate p1 int
axiom h : p1 n
goal G : p n
```

```whyml
constant n : int
predicate p int
predicate p1 int
axiom h : p1 n
axiom Init : n <= 0
goal G : p n
```

```whyml
constant n : int
predicate p int
predicate p1 int
axiom h : p1 n
axiom Init : 0 < n
axiom Hrec : forall n1:int. n1 < n -> p1 n1 -> p n1
goal G : p n
```

--------------------------------

### Launch Why3 GUI

Source: https://why3.org/doc/_sources/starting.rst.txt

Launch the Why3 GUI on the hello_proof.why file.

```text
why3 ide hello_proof.why
```

--------------------------------

### OCaml setup for building WhyML untyped syntax tree

Source: https://why3.org/doc/api.html

Initializes Why3 configuration, environment, and opens Ptree and Ptree_helpers modules. Required before constructing programmatic WhyML modules.

```ocaml
open Why3
let config : Whyconf.config = Whyconf.init_config None
let main : Whyconf.main = Whyconf.get_main config
let env : Env.env = Env.create_env (Whyconf.loadpath main)
open Ptree
open Ptree_helpers

```

--------------------------------

### why3 config add-prover: syntax and example

Source: https://why3.org/doc/_sources/manpages.rst.txt

The first line shows the general syntax for manually registering a prover. The second line is a concrete example that adds an Alt-Ergo executable with the shortcut 'new-ae'. Manually added provers are stored under [partial_prover] sections with manual = true.

```text
why3 config add-prover <name> <file> [<shortcut>]
```

```text
why3 config add-prover Alt-Ergo /home/me/bin/alt-ergo-trunk new-ae
```

--------------------------------

### Module Import and Setup

Source: https://why3.org/doc/whyml.html

Initial module declaration and imports for the InvertingAnInjection module.

```WhyML
module InvertingAnInjection
  use int.Int
  use array.Array
```

--------------------------------

### intros n, m example

Source: https://why3.org/doc/technical.html

Applies the intros transformation with arguments n and m to a goal with three universal quantifiers, introducing the first two as constants and leaving the third in the goal.

```why3
predicate p int int int
goal G : forall x:int, y:int, z:int. p x y z

```

```why3
predicate p int int int
constant n : int
constant m : int
goal G : forall z:int. p n m z

```

--------------------------------

### Run Why3 IDE with Isabelle server

Source: https://why3.org/doc/itp.html

Launch Why3 IDE with the Isabelle server for the example in examples/logic/genealogy. The server must already be running.

```bash
isabelle use_server why3 ide genealogy

```

--------------------------------

### Start MaxAndSum module

Source: https://why3.org/doc/_sources/whyml.rst.txt

Starts a new module MaxAndSum in the file max_sum.mlw.

```whyml
module MaxAndSum
```

--------------------------------

### Start EinsteinHints theory

Source: https://why3.org/doc/_sources/whyml.rst.txt

Starts the EinsteinHints theory by importing the Einstein theory.

```whyml
theory EinsteinHints
      use Einstein
```

--------------------------------

### intros_n 2 example

Source: https://why3.org/doc/technical.html

Applies the intros_n transformation with argument 2 to a goal with three universal quantifiers, introducing the first two as constants and leaving the third in the goal.

```why3
predicate p int int int
goal G : forall x:int, y:int, z:int. p x y z

```

```why3
predicate p int int int
constant x : int
constant y : int
goal G : forall z:int. p x y z

```

--------------------------------

### Start Einstein theory

Source: https://why3.org/doc/_sources/whyml.rst.txt

Starts the Einstein theory that will contain all individuals of the puzzle.

```whyml
theory Einstein
```

--------------------------------

### intros: Goal before and after introducing quantifiers

Source: https://why3.org/doc/_sources/technical.rst.txt

Shows the goal before and after applying intros n, m. The transformation introduces universal quantifiers into the context as constants.

```whyml
predicate p int int int
goal G : forall x:int, y:int, z:int. p x y z
```

```whyml
predicate p int int int
constant n : int
constant m : int
goal G : forall z:int. p n m z
```

--------------------------------

### Install LablGtk3 packages (Debian)

Source: https://why3.org/doc/_sources/install.rst.txt

Install the LablGtk3 and LablGtkSourceView3 OCaml libraries for the graphical interface.

```shell
liblablgtk3-ocaml-dev liblablgtksourceview3-ocaml-dev
```

--------------------------------

### Initialize Why3 configuration and environment

Source: https://why3.org/doc/api.html

Initializes the Why3 configuration and environment, as described in Section 11.3. This is the first step to build an environment for the typed declaration examples.

```ocaml
open Why3
let config : Whyconf.config = Whyconf.init_config None
let main : Whyconf.main = Whyconf.get_main config
let env : Env.env = Env.create_env (Whyconf.loadpath main)

```

--------------------------------

### Run configuration phase

Source: https://why3.org/doc/install.html

Starts the configuration phase, which analyzes the current configuration and checks if requirements hold.

```bash
./configure

```

--------------------------------

### Install OCaml compiler packages (Debian)

Source: https://why3.org/doc/_sources/install.rst.txt

Install the OCaml compiler and native compiler packages on Debian-based Linux.

```shell
ocaml ocaml-native-compilers
```

--------------------------------

### Session statistics output for --session-stats

Source: https://why3.org/doc/_sources/manpages.rst.txt

Example output of the --session-stats option on the "hello proof" example. It shows root and sub-goal counts, unproved goals, goals proved by only one prover, and per-prover statistics including proof attempts, successes, and min/max/average time in seconds.

```text
== Number of root goals ==
  total: 3  proved: 2

== Number of sub goals ==
  total: 2  proved: 1

== Goals not proved ==
  +-- file [../hello_proof.why]
    +-- theory HelloProof
      +-- goal G2
        +-- transformation split_goal_right
          +-- goal G2.0

== Goals proved by only one prover ==
  +-- file [../hello_proof.why]
    +-- theory HelloProof
      +-- goal G1: Alt-Ergo 2.1.0
      +-- goal G2
        +-- transformation split_goal_right
          +-- goal G2.1: Alt-Ergo 2.1.0
      +-- goal G3: Alt-Ergo 2.1.0

== Statistics per prover: number of proof attempts, successful ones, time (minimum/maximum/average) in seconds ==
  Alt-Ergo 2.1.0                :     5     3   0.00   0.00   0.00
  Coq 8.11.2                    :     1     0   0.00   0.00   0.00
```

--------------------------------

### simplify_recursive_definition example: before and after

Source: https://why3.org/doc/technical.html

Reduces mutually recursive definitions if they are not really mutually recursive. The example shows a definition before and after the transformation.

```why3
function f : ... = ... g ...
with g : ... = e

```

```why3
function g : ... = e
function f : ... = ... g ...

```

--------------------------------

### Example usage of --sub-goal

Source: https://why3.org/doc/manpages.html

Demonstrates how to use the --sub-goal option to target specific preconditions in a Why3 file.

```bash
why3 prove --sub-goal=:123@Precondition file.mlw
```
Tokens:
Raw