Principles of Contract Languages

It is one thing to discover that the conditions stipulated by a contract have been violated –but it is another thing to provide an explanation for this violation. And what is an explanation anyway? In this short talk, we explored the notion of explanation for specifications expressed on event streams, and showed how an existing event stream processing engine called BeepBeep has been retrofitted to automatically compute explanations for the violation of a specification.

In this talk, I have started with a brief history of model checking, introduced the general idea, and sketched some major achievements that have significantly increased the feasibility of model checking over the years. Then, I have presented two examples from our own work where we have applied model checking to embedded systems: An approach where we proposed automated partitioning of hardware/software co-designs and then model checked the partitions, and another approach where we proposed to use contracts for the safe integration of reinforcement learning into embedded control systems. I have discussed some ideas we had for modular verification that actually enabled us to verify complex systems, but I also demonstrated where we failed and where I think introducing a notion of contracts into the verification process would be beneficial, if good abstractions and constructs to express these abstraction were available.

Parallelization of programs relies on sound and precise analysis of data dependences in the code, specifically, when dealing with loops. State-of-art tools are based on dynamic profiling and static analysis. They tend to over- and, occasionally, to under-approximate dependences. The former misses parallelization opportunities, the latter can change the behavior of the parallelized program. We have developed a sound and highly precise approach to generate data dependences based on deductive verification. The central technique is to infer a specific form of loop invariant tailored to express dependences. To achieve full automation, we adapt predicate abstraction in a suitable manner. To retain as much precision as possible, we generalized logic-based symbolic execution to compute abstract dependence predicates. We implemented our approach for Java on top of a deductive verification tool. The evaluation shows that our approach can generate highly precise data dependences for representative code taken from HPC applications.

Contract-based formal specification languages are popular in deductive verification, runtime verification and, increasingly, in model checking and test case generation. We outline the building blocks of contract languages and trace some historical developments, as well as current usage. Finally, we suggest some research challenges:

1. 1.

   Sub-procedural contracts

   • $\mathrm{■}$

     blocks, loops, suspension points, barriers

2. 2.

   Combine trace-based specification for global properties
   with lossless contracts for recursive procedures

3. 3.

   Rethink abstract vs. implementation-layer specs

4. 4.

   Contracts for concurrent languages

5. 5.

   Contract composition

6. 6.

   Unify contracts for deductive & runtime verification and testing

7. 7.

   (Behavioral) types as lightweight contracts

8. 8.

   Where do contracts come from? Contract synthesis

9. 9.

   Contract validation, connect to natural language

10. 10.

    Contracts for refinement (correctness by construction)

11. 11.

    Contracts for relational properties

12. 12.

    Debugging contracts

13. 13.

    Domain-specific contract languages

So far, I have used software verifiers to check functional equivalence of two programs, the original and refactored one. To this end, I split the check for functional equivalence into one check for each refactored code segment [1] (code segments are identified by the user). Each check of a refactored code segment inspects the functional equivalence of original and refactored code segment. Therefore, I encode the check of each refactored code segement into a separate verification task. In this talk, I will look into an alternative to describe the verification task, namely contracts. This may allow us to use other tools, e.g., deductive verifiers to check the equivalence of the two code segments.

Semantically lIfted programs [1] enable programs to explicitly refer to their own program state as a knowledge graph, and add information about the application domain through the integration of ontologies. This talk discussed the challenges and chances for contracts in this setting: using ontologies, we can formulate contracts using domain knowledge together with the domain expert, yet stay in a fully formal setting thanks to the rich theories developed the semantic web. However, the questions how exactly to (a) connect with these theories, and (b) how to use languages for data access, such as SPARQL, in a contract language beyond simple typing guarantees [2] remain open.

Formal verification of real-life industrial software remains a challenging task. It provides strong guarantees of correctness, which are particularly important for security-critical products, such as smart cards. Security of a smart card strongly relies on the requirement that the underlying JavaCard virtual machine ensures necessary isolation properties. This talk presents a recent formal verification of a JavaCard Virtual Machine implementation performed by Thales for Common Criteria certification using the Frama-C verification toolset. The certification was successful: an EAL6 certificate was delivered in October 2021 and an EAL7 certificate (the highest one) was delivered in October 2022. This is the first verification project for such a large-scale industrial smart card product where deductive verification is applied on the real-life C code. The target properties include common security properties such as integrity and confidentiality. The implementation contains over 7,000 lines of C code. After a formal specification in the ACSL specification language, over 50,000 verification conditions were generated and successfully proved. We give an overview of the project and proof results, and focus on the mataproperty based approach that was a key solution for a successful specification and verification of security properties. This is a joint work with Adel Djoudi and Martin Hána.

Major safety-critical systems, like the NASA Lunar Gateway Vehicle System Manager, utilize structured English requirements (called contracts) with strict requirements for validation and traceability from early design time through system runtime. We overview the successes and challenges of this approach, highlight recent work in automated temporal logic contract validation, and point out the most immediate needs for future research.

Existing arbitrary first-order (FO) formula evaluation approaches are less efficient than the established algorithms based on finite tables which are used in existing database management systems. However, latter cannot handle arbitrary FO formulas, but rather those that have a particular syntactic structure, e.g., isomorphic to relational algebra expressions.

I will showcase a new translation from arbitrary FO formula into two relational algebra expressions for which the finiteness of the formula’s evaluation result is guaranteed. Assuming an infinite domain, the two expressions have the following meaning: The first is closed and characterizes the original formula’s relative safety, i.e., whether given a fixed database, the original formula evaluates to a finite relation. The second expression is equivalent to the original formula, if it is relatively safe. The translation improves the time complexity over existing approaches, which we also empirically confirm in both realistic and synthetic experiments.

This talk investigates what annotations are actually needed for deductive verification, and provides a taxonomy to categorise these annotations. In particular, we identify several top-level categories, which are further divided into subcategories of annotations. This taxonomy is then used as a basis to investigate how often particular annotation categories occur, by inspecting over 10k lines of annotated programs. To determine whether the results are in line with expectations, we have interviewed several experts on deductive verification. Moreover, we show how the results can be used to evaluate the effectiveness of annotation generators. The knowledge from this analysis provides a gateway to guide further research in improving the efficiency of deductive verification, e.g.: it can serve as a guideline on what categories of annotations should be generated automatically, to evaluate the power of existing annotation generation techniques, and to improve the teaching of deductive verification.

In our view, the primary purpose of contracts is to split responsibilities, and assign them to different parts of a system. To this end, we propose an abstract view of contracts as the formal foundation. Treating contracts as mathematical objects enable elegant formalisation of their properties, while also allowing artefacts of existing formalisms and tools to be cast in the theory.

We discuss our work on a contract theory, based in this principle. The contract theory is aimed at procedural, embedded software, and adheres to established desired properties in system design. It is defined only at the semantic level, in a denotational style. It is also parametrised on the semantic domain, enabling the instantiation of different semantics for particular uses. Previously, we have verified industrial embedded software deductively, with the goal of ensuring functional correctness of low-level system components. Recently we are also interested in high-level system properties, typically of a temporal nature. Because of the abstract view taken of contracts, both of these notions fit naturally into our framework.

We overview the structure of contracts languages used for specifying code for static verification. We report on our experience of using the Dafny Language in teaching software verification at both undergraduate and postgraduate level at Maynooth University; using Dafny to complete verification challenges in our research groups; and our experience of similar tools which have participated in the VerifyThis verification competition series over the past decade.

Contracts in static verification focus on modular specification of code. We present a range of examples and exercises with specification contracts consisting of pre-conditions, post-conditions and frame conditions, indicated by the requires, ensures and modifies clauses respectively. We discuss under-specification and over-specification in contracts, directing discussion to what is meant by contract verification. We note that verification proofs often require more information that that provided in the method contracts. This includes information expressed as assertions (assert), loop and class invariants (invariant), termination metrics (decreases) and specification-only ghost code, as well as using built-in data types (set, sequence, multiset etc.) which provide abstraction and support for verification. We discuss their role in both the specification contracts for the code, and in the contracts which verification tools use during the proof of correctness. Finally, we summarise how we view contract’s in static verification and present future challenges for contract languages and static verification tools as the way that we build and verify software evolves.

This survey talk considers software contracts, consisting of pre-conditions and post-conditions, for imperative programs. Contracts of this kind enable modular verification of programs, and are therefore an important tool to scale up verification methods to large code bases. Formulating sufficient contracts is a time-consuming process, however, making the possibility to compute contracts automatically an attractive option. After studying the algebraic structure of software contracts, the talk surveys some of the contract inference methods that have been proposed in the literature. Considered contract inference methods derive contracts from programs implementations and program specifications, and can produce auxiliary annotations that complement manually written specifications.

The talk is partly based on recent joint work with Anoud Alshnakat, Jesper Amilon, Zafer Esen, Dilian Gurov, and Christian Lidström.

Frame conditions of the form $x^{\prime }=x$ are essential for pre/post condition contracts to specify the parts of a state that remain unchanged under execution of an operation. Though seemingly trivial equations, frame conditions are a common source of error in specifications of industrial systems, in particular when they need to be propagated through several levels of abstraction. The talk discusses common yet expensive error patterns and an approach to debug erroneous frame specifications.

Correctness-by-Construction (CbC) is an incremental software development technique to create functionally correct programs guided by a specification. In contrast to post-hoc verification, where the specification and verification mainly take part after implementing a program, with CbC the specification is defined first, and then the program is successively created using a small set of refinement rules. This specification-first approach has the advantage that errors are likely to be detected earlier in the design process and can be tracked more easily. Even though the idea of CbC emerged many years ago, CbC is not widespread and is mostly used to create small algorithms. We believe in the idea of CbC and envision a scaled CbC approach that contributes to solving problems of modern software development. In this presentation, I will give an overview of our work on CbC in four different lines of research. For all of them, we provide tool support building the CorC ecosystem that even further enables CbC-based development for different fields of application and sizes of software systems.

We present VeyMont: a deductive verification tool that aims to make reasoning about functional correctness and deadlock freedom of parallel programs (relatively complex) as easy as that of sequential programs (relatively simple). The novelty of VeyMont is that it “inverts the workflow”: it supports a new method to parallelise verified programs, in contrast to existing methods to verify parallel programs. Inspired by methods for distributed systems, VeyMont targets coarse-grained parallelism among threads (i.e., whole-program parallelisation) instead of fine-grained parallelism among tasks (e.g., loop parallelisation).

During the plenary discussions in the seminar it was universally agreed that the ability to specify data structures at a suitably abstract, implementation-independent level is crucial to keep specification and verification effort of complex programs manageable. At the same time, the abstraction mechanisms offered by contemporary contract languages are insufficient to achieve this goal.

In addition to feasibility of the specification and verification effort, the capability to abstract away from implementation details in specifications has further important advantages: (i) Better communication with stakeholders at their level of abstraction, (ii) encouragement to write abstract specifications first, (iii) independence from implementation language (multi-language support), (iv) independence from a specific implementation.

In consequence, the breakout group was tasked to explore what kind of abstraction mechanisms might be required and suitable.

Consider a piece of client code that intends to use the implementation of a given API. For example, the client needs to manage a set of objects of a certain type. Most languages offer an API for managing collections of objects, including sets. For efficiency reasons, sets are implemented with mutable data structures, such as arrays or linked lists. But this makes it problematic to specify the intended behavior at the abstract level, i.e. in terms of sets, because separation properties are specified at the implementation level and also differ among different implementations. In addition, one must make sure that the usage of the API by the client does not break memory separation.

In consequence, we need a discipline and mechanisms that encapsulate separation properties and that ensure their preservation at an abstract level. Current mechanisms as realized in languages such as Dafny or JML are based on represents clauses that define how abstract specification elements can be implemented in terms of concrete ones. While it is certainly essential to provide such representations, this is not sufficient to achieve abstraction in the sense outlined above for a number of reasons:

• $\mathrm{■}$

  The relation between abstract elements and the read/write footprint of concrete ones is not explicit, which is necessary to compute and verify assumptions.

• $\mathrm{■}$

  Represents clauses that relate to the same abstract datatype are not grouped together and named.

• $\mathrm{■}$

  There is no control over the visibility of the implementing elements.

• $\mathrm{■}$

  There are no specification constructs that permit to express under which conditions a given property of an abstract specification is preserved under a given operation.

In consequence of the above considerations, we propose the concept of an abstract type.⁶⁶6Their might be a better terminology, this is just a working proposal. This is not a type of the underlying implementation language and outside its type hierarchy. Rather, we are thinking of a trait-like structure that might look as follows:

This defines an abstract type $T^a$ parameterized with some object type P (which we omit in the following for brevity). It provides

1. 1.

   the representation of a $T^a$ object in terms of concrete implementing types $T_1^c,\mathrm{\dots },T_n^c$, together with invariants that define what a valid instance is, for example, the property that a set is idempotent. The predicate ${\text{Valid}}_{T^a}(V^a)$ expresses that $V^a$ is a valid value of $T^a$.

2. 2.

   a set of pure operations that do not change the state and which can be used in assertions.

3. 3.

   a set of impure operations.

4. 4.

   a subset of pure and impure operations to be used as building blocks in abstract specifications. The remaining operations and the definitions are opaque.

Let us call the relation between abstract and concrete types as sketched above a coupling. We will also need to define abstract properties that relate one or more abstract object:

Abstract properties are domain-specific and should be defined in connection with a given abstract type. Examples of properties are: separation, reachability, order, containment, etc.

We illustrate how this setup can be used to simplify verification of concrete types, i.e. the implementation of an abstract type. Consider the bottom row in Fig. 3, representing the following contract of a concrete implementation of function $f^c$:

Assume we want to prove this contract without referring to the concrete implementation as much as possible. We can assume that the corresponding abstract contract for $f^a$ (analogous to $f^c$) has been shown already. Moreover, we can assume the coupling relation

to be given. The corresponding relation $R_{\text{post}}$ can be computed using the implementation of $f^c$.

Now we establish the preservation property for pre and post:

If the properties are chosen well and with the help of some composition theorems, this needs to be shown only once.

This should be sufficient to establish the concrete contract of $f^c$, i.e. the following should be provable as a meta theorem:

Obviously, this is just a sketch, not a formal proof. To go further, we need to instantiate the schema for specific frameworks and look at a concrete example.⁷⁷7During the breakout sessions, Alexander Summers sketched how a similar setup might look in the Viper framework. Notably, it must be clarified in which way our proposal generalizes model fields and methods. The meta theorem(s) must be formally proven, the assumptions clarified, etc.

Besides this, there are several open questions:

• $\mathrm{■}$

  What are minimal assumptions to make this work? Can the equivalence in eqs. (1), (2) be relaxed?

• $\mathrm{■}$

  What are the links to the B-method, as well to abstract interpretation?

• $\mathrm{■}$

  We assumed that the footprints of the $V_i^c$ are disjoint – can it be generalized?

• $\mathrm{■}$

  To be practicable, the framework sketched here should be supported by specification idioms and patterns.

We document the outcome of the break-out sessions on Specification Engineering, held at the Dagstuhl Seminar on Principles of Contract Languages, November 2022.

We identify two main activities in engineering the (formal) specification of a system component or unit: a) the coming about of some first version of a specification, and b) developing existing specifications further, by maintenance, correction, refinement, extension, and alike. Activity a) refers to the initial formalization of the component’s requirements, which could be based on natural language descriptions, on the specifiers own understanding of the requirements, or other sources. While this is a very relevant problem, it has not been the focus of our discussions, and is not what this summary contributes to. Instead, we focus entirely on b), i.e., the activity on assessing the quality of a given status of the specification, and developing it further accordingly.

Specifications ought to represent certain desired properties of the system, typically as constraints, postulates, and models of the behavior. Those should be more obviously correct than the code itself, and should sufficiently describe the guarantees that other components rely on.

Large parts of the realm of formal methods is devoted to providing formal evidence that a system or component actually implements its specification, through mechanized verification. As of yet, much less focus is given to providing evidence on the correspondence between intended requirements and the formal specification, even if there is high demand on addressing this issue. Accordingly, we are interested in the correspondence between the mental model inside the head of developers and the model that is actually formalized as by the specification. Moreover, we are interested in the correspondence between the what properties other components require, and what the specification of this component actually guarantees.

While there are some established techniques, e.g. from the area requirements validation such as illustrating the meaning of temporal logic formulas, we seek to integrate these into a general framework that supports a systematic tool-driven process to ensure the aforementioned correspondences. Therefore, our research goal is

• $\mathrm{■}$

  to bridge between the mental model of the system’s intended behavior and the formalized specification, and

• $\mathrm{■}$

  to bridge between requirements assumed by other components, and the guarantees provided by this specification.

We have identified the following main questions.

• $\mathrm{■}$

  How is the process driven? E.g., which (kinds of) questions should the developer be able to pose to the system’s specification to get a better understanding, and similarly, which questions should be derived from the specification to be posed to the developer?

• $\mathrm{■}$

  What are the different dimensions and artifacts over which this dialogue is formulated and how can we ensure that these have a formally precise meaning while at the same time being easy to understand?

• $\mathrm{■}$

  What tools exists today that can be leveraged at which stages of the process?

• $\mathrm{■}$

  What tools (or tool functionalities) are yet to be provided by the community in the course of realizing such a process?

To address the bridge between the mental model of the system’s intended behavior and the formalized specification, we propose to use an iterative approach similar to active learning, see Figure 4.

The main idea behind this approach is that the user can iteratively improve upon the existing specification by using different tools and techniques to gain a better understanding of the current specification, and develop it further accordingly. Similarly, the context in which the system is used can use a similar approach to enforce limitations of the system’s context. Focusing on the relation of the user’s mental model and the specification for now, the approach caters for tool supported querying in two directions. In the one direction, the user can post queries, to be answered by tools analyzing the specification. These answers shall help the user to evaluate how well the specification matches her own mental model of the component. In the other direction, tools can generate queries to the user, for instance by deducing consequences of the specification. The user can “answer” the query by indicating whether the that consequence matches the intention. Also, tools can question the use of a common logical fallacies, anti-patterns, inconsistencies or vacuously true parts of the specification.

When asking questions to the user in this setting, it is important to take a few things into account. Firstly, one should ask the most important questions first. To achieve this one could use dynamic question prioritization. Secondly, one should be efficient with the questions that are asked to avoid overburdening the user. Finally, one should ask both positive and negative questions.

Some examples of techniques that can be used in this active learning setting to gain a better understanding of the specification are exemplified below. These techniques are well-known and their integration into our method will benefit from advances in the respective research areas.

Generating models of specifications helps to make concrete what specifications mean. The existence of models in the first place rules out vacuous specifications, i.e., formalizations that admit no behavior at all (e.g. an unsatisfiable precondition renders a method contract vacuously true) or that trivially allow all behaviors. Such models have a wide variety of uses cases, cf. below, and can be generated with the help of modern SAT/SMT solvers.

Visualization is a powerful tool that helps to illustrate the meaning of specifications. This has notably been explored for temporal logic formulas, where e.g. input signals for cyber-physical systems can be generated automatically and presented side-by-side with the corresponding outputs. Such a visual presentation has the advantage that it is very easy for a human to assess whether it matches their mental model.

The original formulation of the specification as provided by the engineer can be transformed symbolically and re-phrased by automated tools. Examples are the simplification and normalization of formulas and the computation of logical consequences and lemmas via theory exploration. This help to clarify what the specification means in the general sense, in contrast to examples which can only cover concrete cases.

Linter-like checks can be used to discover typical formalization mistakes. For instance, a universal quantifier should always be paired with an implication and an existential quantifier should be paired with a conjunction, as an example, the formula $\exists x.x\in P⟹Q(x)$ almost certainly does not express the engineer’s intention. Such checks can be integrated with a database of typical specification patterns and anti-patterns. Another example are typical liveness and safety properties in temporal logic.

Mutation testing is technique that attempts to discover the effect of changing the specification in certain “typical” ways (e.g. to replace an occurrence of by $\le$). In software testing this is applied to assess the robustness of test-suites, here it can similarly be used to discover whether such mutations are in conflict with some insights learned already as evidence that the correspondence between the mental model and the specification has been exercised in sufficient detail to notice the mutation at all.

This approach can be used for many different types of specifications, e.g. pre-/postcondition style contracts, temporal logic formulas, or test cases. Depending on the type of specification that you are interested in, different techniques will be available in this iterative approach.

In order to move forward in the direction of realizing the method sketched above, one should survey existing tools for analyzing specifications and answering queries about them. Equally important would be an investigation on what kind of queries (and their according answers) would help users to judge the extent to which a current specification matches the mental model.

A proof of concept for the proposed method could be to instantiate the approach with at least two concrete ways, e.g., with tow tools supporting to query pre/post-specifications or trace-based specifications, respectively. Those shall then be applied to a few small case studies to begin with. This will help to demonstrate how current methods and tools can already support such a process and where gaps and weaknesses are.

This document summarises the discussions of the break out session on Interoperable Contracts held at the Dagstuhl Seminar on Principles of Contract Languages.

The current status in research on contracts is that there is a versatile set of tools for verifying software, but these tools cannot be used interchangeably. We explore what would be needed to achieve interoperability. Specifically, our research question is:

What contract infrastructure is needed to allow tools to interoperate w.r.t. formal contracts?

We consider this question for a wide range of tools. Besides tools using pre- and postcondition contracts, we also include tools with other notions of contracts for software. A motivation for including these tools is that they also target verification of software. In Table 1 we list the research areas of the type of tools we consider. For each area, we state the most important ‘types’ of contract, i.e. what needs to be specified to enable the software verification. Additionally, the table lists the mode of operation: is software analysed statically, or at run-time, so dynamically.

From the overview of Table 1 we selected two specific interoperability cases:

Pre-postcondition contracts only

Interoperability for two deductive verification tools, or a deductive verification and a run-time assertion checking tool, using pre- and postcondition contracts as specification language.

Different contract types + static-dynamic

Interoperability between a deductive verification tool and a dynamic verification tool using automata and/or temporal logic specifications.

Next, we enumerate the main challenges that we identified for interoperability between deductive verification tools and run-time assertion checkers, using pre- and postcondition contracts as specification language.

Contract language and translation.

Tools use languages with different syntax and semantics. Translation from one tool language to the other is needed to make tools interoperable. A promising direction is to design a common or unified language for contract exchange, though this could be “too late now” with the current diverse landscape.

Executable static languages.

There are tools with languages that can be used for both static and dynamic verification of pre-postcondition contracts, e.g. the E-ACSL language component of ACSL in tool Frama-C, and the language of the tool Spark have been designed such that all specifications can be used for static verification, but are also executable for run-time verification. However, this requires that the static and dynamic semantics of the assertions coincide, which makes it challenging.

Implicit assumptions.

When exchanging verification tasks, implicit assumptions need to be taken into account, as an assumption can change the semantics of a contract. We distinguish three types of differences in assumptions:

• $\mathrm{■}$

  Differences in semantics that do not cause any issue for the combination. For example, one tool does not verify exceptional behaviour like run-time exceptions, so it must be ensured that this part is verified by another tool that is able to do this.

• $\mathrm{■}$

  Differences that need to be made explicit in the pre/postcondition, but still allow the interaction to take place. For example, if one tool assumes that objects are non-null, then an explicit assertion can be used in another tool without this assumption.

• $\mathrm{■}$

  Different constructs that must be disallowed because they are handled in a different way by the two tools. For example, different semantics for floating point numbers are used in two different tools, so the verification result is different for the two tools.

Division of the verification task.

To be able to use the interoperability of tools, we need a method for dividing the verification task. Here, the contract, the code, or both could be divided in pieces for distribution to different tools.

Coordinating tool interoperability.

It needs to be decided, either manually or automatically, which tool verifies what. Note here that to be able to use different tools effectively, an explicit overview or mapping of tool capabilities is needed, to know which parts or properties need to be verified by which tool for obtaining the most optimal (e.g. most conclusive or most time-efficient) verification result.

Combining verification results.

The verification results of the used tools need to be combined to one global verification result saying what was (not) proven. Used assumptions need to be included in this result. Also, in case of verification failures, it must be possible to to trace back the failures for analysis and modification purposes.

Application to multi-language software.

A software system may consist of multiple languages. Verifying this with a single verification tool is already challenging.

Below we list approaches for interoperability between a tool using contracts, and a tool using automata and/or temporal logic. We note that most approaches can be found in the existing literature and that static-dynamic interoperability may be coordinated in both directions.

Outsourcing.

A deductive verifier could outsource difficult-to-prove conditions to a (runtime) monitor or assertion checker, or a runtime monitor could outsource difficult-to-monitor conditions to a deductive verifier.

Monitor reduction.

Deductive verification or model checking can be used to check properties such that monitoring assertions can be removed. For example, one might omit monitoring a part of a temporal logic formula because it has been proven via static verification.

Contracts for abstraction hierarchy.

One may replace a subcomponent of an automaton by a pre- post condition contract or a temporal logic formula and use a model checker to verify this abstraction step.

Contracts for automaton actions.

One may use an automaton to model the sequences of method calls, where a method corresponds to a transition, specified by a contract: the precondition is the guard of the transition, and the postcondition the action or resulting state change.

Correspondence checks between automaton and code via annotations.

One may translate an automaton to annotations in the program to prove correspondence between the automaton and the code.

Verification of unbounded data in testing.

One may use deductive verification to abstract from unbounded data parameters in an automaton used for test generation.

Several of the participants in the working group would like to explore the interoperability of tools that use pre- and postconditions as contracts more. They plan to discuss more about these different categories of implicit assumptions, and whether these could be identified in a systematic manner.

For the combination of static and dynamic verification techniques with different contract types, the results were more inconclusive. It is an interesting area, with a high potential, but we need further discussions to come up with concrete new ideas on how to exploit this combination.