Slang is designed to support highly automated verification as an integral part of a developer’s source code authoring, debugging, and testing activities.

To enable this vision, developers need some way of precisely specifying properties that they want to hold for their code. Ideally, the property specification notation needs to be familiar to developers, and viewable and editable within the same tools that are using to develop code. Moreover, developers need to be able to easily associate the specifications to the code to which they apply.

To support these objectives, Slang provides program annotations that developers use to state property specifications in their source code. The specification annotations are similar to other source-code-level specification frameworks such as SPARK Ada, Microsoft’s Code Contracts, Dafny, the Java Modeling Language (JML), add additional references. Slang specification annotations are designed to support an automated verification process based on Floyd/Hoare Logic – an approach for reasoning about programs whose princples reach back to the 1960’s. While early applications of Floyd/Hoare Logic were highly manual, advances over the last two decades in SAT and SMT solvers make it possible to verify complex source code in a highly automated fashion.

Introduce the term for the annotations – “Slang Contract Language”

At present, Slang Contracts are presented in special Scala structures that can be process by a special Sireum extension to the Scala compiler front-end. For example, in the following contract fragment::

  Contract(
      Requires(y > 0),                               
      Modifies(x),                                   
      Ensures(x > In(x)))

Contract, Requires, Modifies, Ensures, and In are all Slang object constructors, and e.g., Requires and Ensures take arguments that are boolean expressions.

In contrast to other contract frameworks that state contracts in a language’s comment syntax, this means that advanced IDE actions such refactoring, code high-lighting, code folding, etc. all apply immediately to contracts. Moreover, language processing of the compiler such as syntax checking, symbol resolution, etc. for contracts is directly integrated with the Scala compiler’s implementation of these tasks. On the negative side, the syntax is a bit less elegant than what one might obtain using a custom grammar for the contract notation.

The Logika Verifier