Hoare-logic-based invariant annotation and automated checking for Fortran.

Annotations

Programs must be annotation in order to check them. Annotations are of the form

Static assertions

!= static_assert keyword (logic_expression)

The possible keywords are

pre

program unit preconditions.

post

program unit postconditions.

seq

invariants between program statements.

invariant

loop invariant annotations.

Logical Expressions

A logical expression is an expression formed from quoted Fortran expressions combined with an arbitrary combination of the logical operators

&

conjunction

|

disjunction

->

implication

<->

bi-implication, equivalence

!

negation

For example,

"x >= 3" & ("y = 7" | "y = z")

is a valid logical expression.

Variables

In logical expressions, you may use any Fortran variables that are declared in the associated program unit, and you may use an annotated function's return variable as long as it has a declared type (i.e. the function's name unless otherwise specified). In addition, you may declare auxiliary variables using the syntax

!= decl_aux("<type spec>" :: <name>)

<type spec>

an arbitrary Fortran type specification, such as integer or real(kind=8,dimensions=(3,4))

<name>

any string (case-insensitive) that is a valid Fortran identifier, such as my_var123.

Using any undeclared variables will result in an error.

Necessary Annotations

Annotations are required at the following program points:

• Between any two statements S1 and S2, where S2 is not an assignment.
• On the line after do ....

Unsupported Program Constructs

Many parts of Fortran are currently unsupported. You will receive a helpful error message if you try to use something that's unsupported. Notable unsupported constructs are:

• Standard do loops (do while loops are supported)
• Multi-dimensional arrays
• User-defined data types
• Program sub-units
• Intrinsic functions
• write, read, etc
• Subroutine and function calls

Example

Here's an example of a properly annotated Fortran program:

!= decl_aux("integer" :: x_)
!= decl_aux("integer" :: y_)
!= static_assert pre("x == x_" & "y == y_")
!= static_assert post("multiply == x_ * y_")
integer function multiply(x, y)
  implicit none

  integer :: x, y
  integer :: r, n

  if (x < 0) then
     x = -x
     y = -y
  end if

  r = 0
  n = 0
  != static_assert seq("x * y == x_ * y_" & "n == 0" & "r == 0" & "n <= x")
  do while (n < x)
     != static_assert invariant("x * y == x_ * y_" & "r == n * y" & "n <= x")
     r = r + y
     n = n + 1
  end do

  multiply = r
end function multiply