https://www.dagstuhl.de/20481

22. – 27. November 2020, Dagstuhl-Seminar 20481

Principles of Contract Languages

Organisatoren

Dilian Gurov (KTH Royal Institute of Technology – Kista, SE)
Reiner Hähnle (TU Darmstadt, DE)
Marieke Huisman (University of Twente – Enschede, NL)
Giles Reger (University of Manchester, GB)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Simone Schilke zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen

Dokumente

Programm des Dagstuhl-Seminars (Hochladen)

(Zum Einloggen bitte persönliche DOOR-Zugangsdaten verwenden)

Motivation

Formal, precise analysis of non-trivial software is a task that necessarily must be decomposed. The arguably most important composition principle in programming is the procedure (function, method, routine) call. For this reason it is natural to decompose the analysis of a program along its call structure. Decomposition in this context means to replace a procedure call with a declarative description, possibly an approximation, of the call's effect. In his seminal work on runtime verification in Eiffel, Bertrand Meyer suggested to use the metaphor of a contract between the user (caller) and implementor (callee) for such a description.

Contracts continue to be a central element in run-time (dynamic) analysis. In the last two decades they also became the dominant decomposition approach in deductive verification and are realized in all major software verification systems. More recently, software contracts are increasingly used in test case generation and model checking. Furthermore, programming languages such as "Racket" were designed with a notion of contract. Contract-based specification languages are available for mainstream programming languages, notably JML for "Java" and ACSL/ACSL++ for "C"/"C++".

However, there is considerable fragmentation concerning terminology, basic principles, expressivity, and usage of contracts in different research communities. Therefore, this Dagstuhl Seminar aims to convene researchers working with contracts in static verification, runtime verification, as well as testing, with the goal of creating a unified view on software contracts.

The seminar will address the following topics and questions:

  • What are the fundamental aspects of contracts for software development?
  • What format or structure should contracts have?
  • How expressive does a contract language need to be?
  • How do contract formats depend on their use cases?
  • How should contracts be composed and decomposed?
  • How can contracts be used for documentation, testing and verification?
  • How can a unified view on contracts help integrating static and dynamic techniques?
  • How can contracts support agile software development?
  • How should contracts be refined upon a failed verification attempt?

The format of the seminar will be as follows. Each day will be dedicated to a specific topic and will consist, in the morning, of one or two tutorials that make a general overview of the topic, followed by short technical talks. During the afternoon, we will have brief pitches from participants to spark off discussions in groups on important questions raised in the morning. The day will be wrapped up by a plenary discussion in which the groups will present a summary of their findings.

Motivation text license
  Creative Commons BY 3.0 DE
  Dilian Gurov, Reiner Hähnle, Marieke Huisman, and Giles Reger

Classification

  • Semantics / Formal Methods
  • Software Engineering
  • Verification / Logic

Keywords

  • Software contract
  • Software specification
  • Static verification
  • Run-time verification

Dokumentation

In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.

 

Download Übersichtsflyer (PDF).

Publikationen

Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.