# 7. Other Input Formats

Why3 can be used to verify programs written in languages other than WhyML. Currently, Why3 supports tiny subsets of C and Python, respectively coined micro-C and micro-Python below. These were designed for teaching purposes. They come with their own specification languages, written in special comments. These input formats are described below.

Why3 also supports the format MLCFG, which is an extension of WhyML allowing to define function bodies in an unstructured style, with goto statements.

Why3 also supports the format Coma (which stands for Continuation Machine). Coma is an Intermediate Verification Language implemented as a plugin in the Why3 platform.

Any Why3 tool (`why3 prove`, `why3 ide`, etc.) can be passed a file with a suffix `.c`, `.py`, `.coma` or `.mlcfg`, which triggers the corresponding input format.

## 7.1. micro-C

Micro-C is a valid subset of ANSI C. Hence, micro-C files can be passed to a C compiler.

### 7.1.1. Syntax of micro-C

Logical annotations are inserted in special comments starting with `//@` or `/*@`. In the following grammar, we only use the former kind, for simplicity, but both kinds are allowed.

    file      ::= decl*
    decl      ::= c_include | c_function | logic_declaration
    c_include ::= "#include" "<" file-name ">"

Directives `#include` are ignored during the translation to Why3. They are allowed anyway, such that a C source code using functions such as `printf` (see below) is accepted by a C compiler.

Function definition

    c_function  ::= return_type identifier "(" params? ")" spec* block
    return_type ::= "void" | "int"
    params      ::= param ("," param)*
    param       ::= "int" identifier | "int" identifier "[]"

Function specification

    spec ::= "//@" "requires" term ";"
             | "//@" "ensures"  term ";"
             | "//@" "variant"  term ("," term)* ";"

C expression

    expr ::= integer-literal | string-literal
             | identifier | identifier ( "++" | "--" ) | ( "++" | "--" ) identifier
             | identifier "[" expr "]"
             | identifier "[" expr "]" ( "++" | "--")
             | ( "++" | "--") identifier "[" expr "]"
             | "-" expr | "!" expr
             | expr ( "+" | "-" | "*" | "/" | "%" | "==" | "!=" | "<" | "<=" | ">" | ">=" | "&&" | "||" ) expr
             | identifier "(" (expr ("," expr)*)? ")"
             | "scanf" "(" '"%d"' "," "&" identifier ")"
             | "(" expr ")"

C statement

    stmt       ::= ";"
                   | "return" expr ";"
                   | "int" identifier ";"
                   | "int" identifier "[" expr "]" ";"
                   | "break" ";"
                   | "if" "(" expr ")" stmt
                   | "if" "(" expr ")" stmt "else" stmt
                   | "while" "(" expr ")" loop_body
                   | "for" "(" expr_stmt ";" expr ";" expr_stmt ")" loop_body
                   | expr_stmt ";"
                   | block
                   | "//@" "label" identifier ";"
                   | "//@" ( "assert" | "assume" | "check" ) term ";"
    block      ::= "{" stmt* "}"
    expr_stmt  ::= "int" identifier "=" expr
                   | identifier assignop expr
                   | identifier "[" expr "]" assignop expr
                   | expr
    assignop   ::= "=" | "+=" | "-=" | "*=" | "/="
    loop_body  ::= loop_annot* stmt
                   | "{" loop_annot* stmt* "}"
    loop_annot ::= "//@" "invariant" term ";"
                   | "//@" "variant" term ("," term)* ";"

Note that the syntax for loop bodies allows the loop annotations to be placed either before the block or right at the beginning of the block.

Logic declarations

    logic_declaration ::= "//@" "function" "int" identifier "(" params ")" ";"
                          | "//@" "function" "int" identifier "(" params ")" "=" term ";"
                          | "//@" "predicate" identifier "(" params ")" ";"
                          | "//@" "predicate" identifier "(" params ")" "=" term ";"
                          | "//@" "axiom" identifier ":" term ";"
                          | "//@" "lemma" identifier ":" term ";"
                          | "//@" "goal"  identifier ":" term ";"

Logic functions are limited to a return type `int`.

Logical term

    term   ::= identifier
               | integer-literal
               | "true"
               | "false"
               | "(" term ")"
               | term "[" term "]"
               | term "[" term "<-" term "]"
               | "!" term
               | "old" "(" term ")"
               | "at" "(" term "," identifier ")"
               | "-" term
               | term ( "->" | "<->" | "||" | "&&" ) term
               | term ( "==" | "!=" | "<" | "<=" | ">" | ">=" ) term
               | term ( "+" | "-" | "*" | "/" | "% ) term
               | "if" term "then" term "else term
               | "let" identifier "=" term "in" term
               | ( "forall" | "exists" ) binder ("," binder)* "." term
               | identifier "(" (term ("," term)*)? ")"
    binder ::= identifier
               | identifier "[]"

### 7.1.2. Built-in functions and predicates

C code

- `scanf` is limited to the syntax `scanf("%d", &x)`.

- `printf` is limited to `printf(string-literal, expr1, ..., exprn)`. The string literal should contain exactly `n` occurrences of `%d` (not checked by Why3).

- `rand()` returns a pseudo-random integer in the range `0` to `RAND_MAX` inclusive.

Logic

- `int length(int a[])` returns the length of array `a`.

- `int occurrence(int v, int a[])` returns the number of occurrences of the value `v` in array `a`.

## 7.2. micro-Python

Micro-Python is a valid subset of Python 3. Hence, micro-Python files can be passed to a Python interpreter.

### 7.2.1. Syntax of micro-Python

Notation: In the grammar of micro-Python given below, special symbols `NEWLINE`, `INDENT`, and `DEDENT` mark an end of line, the beginning of a new indentation block, and its end, respectively.

Logical annotations are inserted in special comments starting with `#@`.

    file      ::= decl*
    decl      ::= py_import | py_constant | py_function | stmt | logic_declaration
    py_import ::= "from" identifier "import" identifier ("," identifier)* NEWLINE

Directives `import` are ignored during the translation to Why3. They are allowed anyway, such that a Python source code using functions such as `randint` is accepted by a Python interpreter (see below).

Constant definition

    py_constant ::= "#@" "constant" NEWLINE identifier "=" expr NEWLINE

Function definition

    py_function ::= logic_def? "def" identifier "(" params? ")" return_type? ":" NEWLINE INDENT spec* stmt* DEDENT
    params      ::= param ("," param)*
    param       ::= identifier (":" py_type)?
    return_type ::= "->" py_type
    py_type     ::= identifier ("[" py_type ("," py_type)* "]")?
                    | "'" identifier

Function specification

    logic_def ::= "#@" "function" NEWLINE
    spec      ::= "#@" "requires" term NEWLINE
                  | "#@" "ensures"  term NEWLINE
                  | "#@" "variant"  term ("," term)* NEWLINE

Python expression

    expr ::= "None" | "True" | "False" | integer-literal | string-literal
             | identifier
             | identifier "[" expr "]"
             | "-" expr | "not" expr
             | expr ( "+" | "-" | "*" | "//" | "%" | "==" | "!=" | "<" | "<=" | ">" | ">=" | "and" | "or" ) expr
             | identifier "(" (expr ("," expr)*)? ")"
             | expr ("," expr)+
             | "[" (expr ("," expr)*)? "]"
             | expr "if" expr "else" expr
             | "(" expr ")"

Python statement

    stmt        ::= simple_stmt NEWLINE
                    | "if" expr ":" suite else_branch
                    | "while" expr ":" loop_body
                    | "for" identifier "in" expr ":" loop_body
    else_branch ::= /* nothing */
                    | "else:" suite
                    | "elif" expr ":" suite else_branch
    suite       ::= simple_stmt NEWLINE
                    | NEWLINE INDENT stmt stmt* DEDENT
    simple_stmt ::= expr
                    | "return" expr
                    | identifier "=" expr
                    | identifier "[" expr "]" "=" expr
                    | "break"
                    | "#@" "label" identifier
                    | "#@" ( "assert" | "assume" | "check" ) term
    loop_body   ::= simple_stmt NEWLINE
                    | NEWLINE INDENT loop_annot* stmt stmt* DEDENT
    loop_annot  ::= "#@" "invariant" term NEWLINE
                    | "#@" "variant" term ("," term)* NEWLINE

Logic declaration

    logic_declaration ::= "#@" "function" identifier "(" params ")" return_type? ("variant" "{" term "}")? ("=" term)? NEWLINE
                          | "#@" "predicate" identifier "(" params ")" ("=" term)? NEWLINE
                          | "#@" "axiom" identifier ":" term NEWLINE
                          | "#@" "lemma" identifier ":" term NEWLINE

Note that logic functions and predicates cannot be given definitions. Yet, they can be axiomatized, using toplevel `assume` statements.

Logical term

    term ::= identifier
             | integer-literal
             | "None"
             | "True"
             | "False"
             | "(" term ")"
             | term "[" term "]"
             | term "[" term "<-" term "]"
             | "not" term
             | "old" "(" term ")"
             | "at" "(" term "," identifier ")"
             | "-" term
             | term ( "->" | "<->" | "or" | "and" | "by" | "so" ) term
             | term ( "==" | "!=" | "<" | "<=" | ">" | ">=" ) term
             | term ( "+" | "-" | "*" | "//" | "%" ) term
             | "if" term "then" term "else term
             | "let" identifier "=" term "in" term
             | ( "forall" | "exists" ) param ("," param)* "." term
             | identifier "(" (term ("," term)*)? ")"

### 7.2.2. Built-in functions and predicates

Python code

- built-in function `pow` over integers

- `len(l)` returns the length of list `l`.

- `int(input())` reads an integer from standard input.

- `range(l, u)` returns the list of integers from `l` inclusive to `u` exclusive. In particular, `for x in range(l, u):` is supported.

- `randint(l, u)` returns a pseudo-random integer in the range `l` to `u` inclusive.

Logic

- `len(l)` returns the length of list `l`.

- `occurrence(v, l)` returns the number of occurrences of the value `v` in list `l`.

### 7.2.3. Limitations

Python lists are modeled as arrays, whose size cannot be modified.

## 7.3. MLCFG

The MLCFG language is an experimental extension of the regular WhyML language, in which the body of program functions can be coded using labelled blocks and goto statements. MLCFG can be used to encode algorithms which are presented in an unstructured fashion. It can also be used as a target for encoding unstructured programming languages in Why3, for example assembly code.

### 7.3.1. Syntax of the MLCFG language

The MLCFG syntax is an extension of the regular WhyML syntax. Every WhyML declaration is allowed, plus an additional declaration of program function of the following form, introduced by keywords `let cfg`:

    let cfg f (x1: t1) ... (xn: tn): t
      requires { Pre }
      ensures  { Post }
    =
     var y1: u1;
     ...
     var yk: uk;
     { instructions; terminator }
     L1 { instructions1; terminator1 }
     ...
     Lj { instructionsj; terminatorj }

It defines a program function f, with the usual syntax for its contract. The difference is the body, which is made of a sequence of declarations of mutable variables with their types, an initial block, composed of a zero or more instructions followed by a terminator, and a sequence of other blocks, each denoted by a label (\(L_1 \ldots L_j\) above). The instructions are semi-colon separated sequences of regular WhyML expressions of type `unit`, excluding `return` or `absurd` expressions, or code invariants:

- a code invariant: `invariant I { t }` where I is a name and t a predicate. It is similar to an assert expression, meaning that t must hold when execution reaches this statement. Additionally, it acts as a cut in the generation of VC, similarly to a loop invariant. See example below.

Each block is ended by one of the following terminators:

- a `goto` statement: `goto L` where L is one of the labels of the other blocks. It instructs to continue execution at the given block.

- a `switch` statement, of the form

      switch (e)
      | pat1 -> terminator1
      ...
      | patk -> terminatork
      end

- a `return` statement: `return expr`

- an `absurd` statement: indicating that this block should be unreachable.

The extension of syntax is described by the following rules.

    file        ::= module*
    module      ::= "module" ident decl* "end"
    decl        ::= "let" "cfg" cfg_fundef
                    | "let" "rec" "cfg" cfg_fundef ("with" cfg_fundef)*
                    | "scope" ident decl* "end"
    cfg_fundef  ::= ident binder+ : type spec "=" vardecl* "{" block "}" labelblock*
    vardecl     ::= "var" ident* ":" type ";" | "ghost" "var" ident* ":" type ";"
    block       ::= (instruction ";")* terminator
    labelblock  ::= ident "{" block "}"
    instruction ::= expr
                    | "invariant" ident "{" term "}"
    terminator  ::=
                    | "return" expr
                    | "absurd"
                    | "goto" ident
                    | "switch" "(" expr ")" switch_case* "end"
    switch_case ::= "|" pattern "->" terminator

### 7.3.2. An example

The following example is directly inspired from the documentation of the ANSI C Specification Language (See [BFM+18], Section 2.4.2 Loop invariants, Example 2.27). It is itself inspired from the first example of Knuth’s MIX language, for which formal proofs were first investigated by J.-C. Filliâtre in 2007 ([Fil07]), and also revisited by T.-M.-T. Nguyen in her PhD thesis in 2012 ([Ngu12], Section 9.5 Translation from a CFG to Why, page 115).

This example aims at computing the maximum value of an array of integers. Its code in C is given below.

    /*@ requires n >= 0 && \valid(a,0,n);
      @ ensures \forall integer j ; 0 <= j < n ==> \result >= a[j]);
      @*/
    int max_array(int a[], int n) {
      int m, i = 0;
      goto L;
      do {
        if (a[i] > m) { L: m = a[i]; }
        /*@ invariant
          @   0 <= i < n && \forall integer j ; 0 <= j <= i ==> m >= a[j]);
          @*/
        i++;
      }
      while (i < n);
      return m;
    }

The code can be viewed as a control-flow graph as shown in Fig. 7.1.

Fig. 7.1 Control-flow graph of the `max_array` function.

Below is a version of this code in the MLCFG language, where label `L` corresponds to node `L`, label `L1` to node `invariant`, label `L2` to node `do`.

    let cfg max_array (a:array int) : (max: int, ghost ind:int)
      requires { length a > 0 }
      ensures  { 0 <= ind < length a }
      ensures  { forall j. 0 <= j < length a -> a[ind] >= a[j] }
    =
    var i m: int;
    ghost var ind: int;
    {
      i <- 0;
      goto L
    }
    L {
      m <- a[i];
      ind <- i;
      goto L1
    }
    L1 {
      invariant i_bounds   { 0 <= i < length a };
      invariant ind_bounds { 0 <= ind < length a };
      invariant m_and_ind  { m = a[ind] };
      invariant m_is_max   { forall j. 0 <= j <= i -> m >= a[j] };
                             (* yes, j <= i, not j < i ! *)
      i <- i + 1;
      switch (i < length a)
      | True  -> goto L2
      | False -> return (m, ind)
      end
    }
    L2 {
      switch (a[i] > m)
      | True  -> goto L
      | False -> goto L1
      end
    }

The consecutive invariants act as a single cut in the generation of VCs.

### 7.3.3. Error messages

The translation from the MLCFG language to regular WhyML code may raise the following errors.

- “cycle without invariant”: in order to perform the translation, any cycle on the control-flow graph must contain at least one `invariant` clause. It corresponds to the idea that any loop must contain a loop invariant.

- “cycle without invariant (starting from I)”: same error as above, except that the cycle was not reachable from the start of the function body, but from the other `invariant` clause named \(I\).

- “label L not found for goto”: there is a `goto` instruction to a non-existent label.

- “unreachable code after goto”: any code occurring after a `goto` statement is unreachable and is not allowed.

- “unsupported: trailing code after switch”: see limitations below.

### 7.3.4. Current limitations

- There is no way to prove termination.

- New keywords `cfg`, `goto`, `switch`, and `var` cannot be used as regular identifiers anymore.

- Trailing code after `switch` is not supported. In principle, it should be possible to have a `switch` with type `unit` and to transfer the execution to the instructions after the `switch` for branches not containing `goto`. This is not yet supported. A workaround is to place the trailing instructions in another block and pose an extra `goto` to this block in all the branches that do not end with a `goto`.

- Conditional statements `if e then i1 else i2` are not yet supported, but can be simulated with `switch (e) | True -> i1 | False -> i2 end`.

### 7.3.5. Alternative translation scheme: Stackify

An alternative translation scheme from MLCFG to regular WhyML can be triggered by putting the attribute `[@cfg:stackify]` on a function. This method attempts to recover a more structured program body, reconstructing loops when possible.

### 7.3.6. Subregion analysis

Additional invariants on the generated WhyML code can be inferred by putting the attribute `[@cfg:subregion_analysis]` on a function. These invariants are derived by a static analysis of the subregions that are never modified in a loop.

## 7.4. S-expressions

This format is intended to be used only as an intermediate language format. Why3 accepts input files in the format of a big S-expression, mirroring the internal structure of parse trees, as they are defined in the module `Ptree` of the OCaml API. The S-expression in question is supposed to be generated by the API itself, that is the function `Ptree.sexp_of_mlw_file`. It is in fact exactly the format that is also printed using `why3 pp --output` with `--output=sexp`.

Notice that this input format is available only when Why3 is compiled with S-expressions support provided by the `ppx_sexp_conv` OCaml library.

Concerning the use of Why3 as an intermediate language, via the `Ptree` API, the use of S-expressions instead of the regular WhyML syntax is recommended since the printing and re-parsing of parse trees is automatically generated, hence the result is guaranteed to faithfully mirror the internal Ptree representation.

## 7.5. Coma

The Coma documentation is described in https://coma-ivl.codeberg.page/.