Responses of HAHA

Error markers

HAHA reports errors by displaying error markers in the editor. Each marker has a tooltip which describes the reason why it was created. List of all errors in a project can be seen in the Problems view, which is shown by default in a tab in the lower pane. It can also be accessed by selecting Window | Show view | Problems from the main menu. This chapter describes various kinds of error markers produced by HAHA.

Syntax errors

Markers for syntax errors are created as the program is typed. No user action is necessary to trigger syntax checking. HAHA syntax is described in detail in section Language reference.

Type errors

Error markers related to typechecking are created and updated only when the source file is saved.

VCGen errors

Error markers are also produced whenever the solver is unable to prove validity of a formula generated from the program. These markers are updated whenever the verification conditions generator is run. Marker description contains context information, which describes why the formula was generated. Example of such information can be seen below:

Verification condition is not valid
  Program correctness
    Correctness of bsearch
      Block at lines 12 - 37
        Loop statement at line 17
          Single iteration preserves invariants.
            Block at lines 21 - 34
              If statement at line 24
                Case 1 - condition holds.
                  Postconditions are valid.
                    still_ordered at line 19

This description tells us that the solver was unable to prove that a loop invariant named still_ordered holds if the first branch of a conditional statement in line 24 is taken.

Verification conditions generator produces error markers in two cases

  • When the solver was able to prove the invalidity of a formula. In this case a counterexample is produced and appended to error description. A counterexample is simply an assignment of values to free varialbes occuring in an expression. For example, an attempt to validate the following program

    function test(x : Z) : Z
      postcondition test >= x
        test := 3 * x
    

    would result in this error:

    Verification condition is not valid
    Program correctness
      Correctness of test
        Postcondition at line 2 (after substitution)
    
    Counterexample:
      x = (- 1)
    
  • When the solver could neither prove nor disprove the formula. This case also covers problems caused by timeouts, internal solver errors and bugs in HAHA.

Warning

Line breaks in error markers are distorted in current version of HAHA. This makes context descriptions and counterexamples harder to read.

Console output

When the verification condition generator is run, a console is displayed in the lower pane. This console logs all messages printed during the process of creating and discharging verification conditions. Messages in the console are more detailed (but somewhat harder to read) than error marker descriptions.

First, all computed verification conditions are printed. Each condition consists of a list of assumptions, followed by a goal. Goal is separated from assumptions by a horizontal line. Note that all expressions are displayed in prefix notation. The following example shows a single verification condition:

n_ge_one : (>= len 1)
orderedA : (CALL-PREDICATE ordered A 1 len)
is_inA : (CALL-PREDICATE is_in A v 1 len)
---------------------------------------------
(AND (= 1 1) (AND (>= len 1) (AND (CALL-PREDICATE ordered A 1 len) (CALL-PREDICATE is_in A v 1 len))))

Declared variables, axioms and predicates are also printed at this stage.

In the second stage, computed conditions are discharged by the solver. During this stage, commands sent to the solver are printed. Possible commands include

  • Declaration of a variable or predicate (DECLARE VAR)
  • New assumption (DECLARE AXIOM)
  • Context management commands MARK and RESET. The latter removes all declarations (both variables and assumptions) since last unmatched occurence of the former.
  • Validity check IS_VALID. This command checks if the goal formula is valid in the current context. After this command, solver response (including a counterexample, if applicable) is printed to the console.

Text lines preceded by >> represent raw text sent to the external SMT solver. Similarly, lines starting with << contain raw solver responses. This is mainly useful for finding bugs related to translation of solver commands to the SMT2 format.