AutoProof Manual

Overview

This manual describes how to use AutoProof. AutoProof is an auto-active verifier for the Eiffel programming language that can prove functional correctness of Eiffel programs annotated with contracts. AutoProof is available as part of the Eiffel Verification Environment (EVE) or via an online version.

AutoProof in EVE

AutoProof is integrated in EVE, a research branch of EiffelStudio.

Installation

Follow the installation instructions of EVE.

Open Project

Open and compile an EiffelStudio project using the EVE base library. For this you can download the example project provided. Launch EVE using the run_eve script in the EVE delivery and add the example's ecf file using the add project button. When you have added the project you can open and compile it.

Open AutoProof tool panel

Click the menu entry View > Tools > AutoProof. This will show the AutoProof panel, which can be docked like the other tools in EVE.

Run AutoProof

The Eiffel compilation of the project has to be finished and successful in order to run AutoProof. It is not necessary to do the C compilation when working with AutoProof. When the project is compiled successfully there are three ways to launch AutoProof:

• You can run AutoProof using the Verify button. By default, AutoProof will verify the class or cluster that is shown in the editor pane. You can change this behaviour by clicking the down-arrow on the Verify button and select either to verify the parent cluster of the item currently shown in the editor, or to verify the whole system (excluding libraries).
• You can pick-and-drop a feature, class, or cluster onto the Verify button.
• You can right-click a feature or class and select Verify with AutoProof in the context menu.

Only one execution of AutoProof can run at a time, so when the verification has started the Verify button will become inactive.

Stop AutoProof

When AutoProof is running you can stop it using the red stop button next to the Verify button. This can be helpful if you want to cancel a long-running verification.

Filtering Results

There are two ways of filtering the results displayed by AutoProof:

• The three toggle-buttons can be used to show or hide all successful results, failed verifications, or semantic errors.
• The filter box can be used to enter text. Only results will be shown where this text is contained in either the class name, feature name, or text message. To clear the filter box you can click the red x button next to it.

Options

On the top-right of the AutoProof tool is the options button. Clicking it will display the available options and if the option is enabled or disabled. Clicking any of the options will toggle its value. For an explanation of the options see the AutoProof Options section.

AutoProof on the Command-line

The command-line version of AutoProof is available as part of EVE.

Run AutoProof

To run AutoProof via the command-line you have to run the EVE command-line compiler with a valid Eiffel project and add the -autoproof option: ec.exe -config ecf-file -target ecf-target -autoproof

By default all user classes in the system are verified by AutoProof. To select which classes or routines are verified you can add the class names and routine names as additional command-line arguments. The routine name is composed of the class name together with the routine in the format CLASS.routine.

Options

AutoProof has the same options on the command-line as for the graphical version. The available command-line options are listed in the AutoProof Options section.

AutoProof on the Web

The online version of AutoProof is integrated in ComCom, an online interface to run command-line tools.

Examples

Across the top of the AutoProof interface on Comcom are different examples that can be selected. The examples can be adapted in the browser. To reload the original version, click the reload button on the top-right.

Custom code

The last tab More AutoProof can be used to write your own code from scratch. In addition to writing your own code you can use command-line options on this tab. For a list of command-line options see the AutoProof Options section.

Run AutoProof

To run AutoProof click the Run button below the code area. The results will be shown in the box below the button. Note that changing the example will clear the results box. The verification time is limited to 2 minutes, you will get a result or a time-out message after that time.

Limitations

The ComCom version of AutoProof is limited to examples that consist only of one user-defined class. You can use the classes of the EVE version of EiffelBase in your code, in particular the ones defined in the AutoProof base library. It is not possible to add further libraries.

AutoProof Options

There are different options which influence the behaviour of the AutoProof translation and execution as a whole, as opposed to annotations which only affect individual classes or features (see the Annotations section for details). The following table lists these options. The command-line switches usually come in pairs: one switch turns the option on and the other turns it off.

Verification Process

Modularity

AutoProof does routine-level modular verification. Each routine is verified in isolation and only the interface of suppliers are considered during the verification of a routine. A program can only be considered fully verified if all routines are verified individually. By default AutoProof only verifies user-written classes when a program is verified, referenced libraries should be verified separately.

Creation routines

Creation routines in Eiffel double as regular routines and can be called on existing objects. Since routines behave differently depending on whether they are called as a creation routine (the class invariant is not checked on entry and all attributes are set to their default value for creation routines) these routines are verified twice with AutoProof. The feedback of AutoProof will list these routines twice specifying the context of the verification.

Assumptions

It can be useful to temporarily assume a fact that the verifier should use. This helps in debugging failed verifications, e.g. by directing the verifier in a specific branch. You can write an assumption using a check instruction with the special tag assume.

check assume: False end

Skipping classes or routines

You can skip the verification of single routines or classes by adding a note clause.

note
  status: skip

Language Support

The programming language that AutoProof supports is not exactly the standard Eiffel language. Some features of the Eiffel language are not supported, on the other hand custom annotations have been added to increase the expressiveness of the specification language. All custom annotations are valid syntax in standard Eiffel.

Standard Eiffel Support

AutoProof supports a large portion of the Eiffel language. When AutoProof encounters code constructs it does not support, it will try to degrade in a correct but incomplete way in order to verify the surrounding program. In any case, a special message will be displayed. Here is a comprehensive list of supported and unsupported instructions, expressions, and language concepts.

Instructions

          a := b
        

          a.f (x)
        

          check tag: c end
        

          if c then
            ... 
          else 
            ... 
          end
        

          create a.f (x)
        

          debug ... end
        

          inspect a
          when x then ...
          when y..z then ...
          else ...
          end
        

          from ...
          invariant
            tag1: i1
            tag2: i2
          until c
          loop ...
          variant v end
        

          across a as c loop 
            ...
          end
        

          retry
        

Expressions

          a
        

          across set as c all ... end
          across 1 |..| 5 as c some ... end
        

          $
        

          a.call([x])
        

          a.f (x)
        

          if c then x else y end
        

          create {T}.f (x)
        

          create {T}.f (x)
        

          << a, b >>
        

          << a, b >>
        

          "abc"
        

          [a, b]
        

          [a, b]
        

          attached {T} a as x
        

          old a
        

Library support and built-in types

          True
          False
        

          a and b or c
          a implies b xor c
        

          1
          -2
        

          a + b - c
          a * b // c
        

          1.2
        

          a + b - c
          a * b / c
        

          'c'
        

          a + b
          c.to_upper
        

          "abc"
        

          a: SIMPLE_ARRAY [INTEGER]
          create a.make (1, 5)
          a.put (v, 3)
        

Annotations

  note
    status: skip, functional

  note
    status: skip
    status: functional

Class Annotations

          note
            explicit: "all"
        

          note
            explicit: contracts
        

          note
            explicit: observers
            explicit: subjects
            explicit: owns
        

          note
            explicit: wrapping
        

          note
            manual_inv: True
        

          note
            model: f, g
        

          note
            status: skip
        

          note
            theory: "file.bpl"
        

          note
            maps_to: "BoogieType"
        

          note
            type_properties: "BoogieFunction"
        

          note
            where: "BoogieFunction"
        

Feature Annotations

          note
            explicit: "all"
        

          note
            explicit: contracts
        

          note
            explicit: wrapping
        

          note
            maps_to: "BoogieFunction"
        

          note
            guard: True
            guard: False
            guard: "SomeFeature"
        

          note
            inline: True
            inline: 4
        

          note
            manual_inv: True
        

          note
            status: creator
        

          note
            status: dynamic
        

          note
            status: functional
        

          note
            status: ghost
        

          note
            status: impure
        

          note
            status: inline_in_caller
        

          note
            status: lemma
        

          note
            status: skip
        

Precondition and Loop Invariant Functions

          require
            decreases (x)
            decreases ([x, y])
            decreases ([])
        

          require
            modify (Current)
            modify (set)
        

          require
            modify_field ("x", Current)
            modify_field ("x", set)
            modify_field (["x", "y"], Current, set)
        

          require
            modify_model ("x", Current)
            modify_model ("x", set)
            modify_model (["x", "y"], Current, set)
        

          require
            reads (o)
            reads_field ("attr", o)
            reads_model ("attr", o)
        

Commands and Queries

          inv
          other.inv
        

          inv_only ("tag1")
          other.inv_without ("tag2", "tag3")
        

          is_free
          other.is_free
        

          is_fresh
          other.is_fresh
        

          is_open
          other.is_open
        

          is_wrapped
          other.is_wrapped
        

          unwrap
          other.unwrap
          unwrap_all (Current, set)
        

          wrap
          other.wrap
          wrap_all (Current, set)