Online version of Why3, with micro-C input format

This version of Why3 is intended for teaching purposes. Its input format is a tiny subset of C, called "micro-C", described below.

Note: the command-line version of Why3 is also supporting this input format, for files with suffix .c.

Syntax of micro-C

Notation: The grammar of micro-C is given below in extended Backus-Naur Form, using | for alternation, () for grouping, [] for option, and {} for repetition.

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 exor
	      | 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 ";"

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 "[]"

Built-in functions and predicates

C code

Logic

Verifying a program

Click on the gears button to launch the verification. Verification conditions (VCs) then appear in the right panel, in the Task List tab, and Alt-Ergo is run on each of them with a default time limit (that can be set in the Settings menu).

When a VC is not proved, there are several options: