We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: An Abstract Contract Theory for Programs with Procedures

Authors: Christian Lidström, Dilian Gurov (KTH Royal Institute of Technology, Stockholm, Sweden)
Abstract: When developing complex software and systems, contracts provide a means for controlling the complexity by dividing the responsibilities among the components of the system in a hierarchical fashion. In specific application areas, dedicated contract theories formalise the notion of contract and the operations on contracts in a manner that supports best the development of systems in that area. At the other end, contract meta-theories attempt to provide a systematic view on the various contract theories by axiomatising their desired properties. However, there exists a noticeable gap between the most well-known contract meta-theory of Benveniste et al., which focuses on the design of embedded and cyber-physical systems, and the established way of using contracts when developing general software, following Meyer's design-by-contract methodology. At the core of this gap appears to be the notion of procedure: while it is a central unit of composition in software development, the meta-theory does not suggest an obvious way of treating procedures as components.
In this paper, we provide a first step towards a contract theory that takes procedures as the basic building block, and is at the same time an instantiation of the meta-theory. To this end, we propose an abstract contract theory for sequential programming languages with procedures, based on denotational semantics. We show that, on the one hand, the specification of contracts of procedures in Hoare logic, and their procedure-modular verification, can be cast naturally in the framework of our abstract contract theory. On the other hand, we also show our contract theory to fulfil the axioms of the meta-theory. In this way, we give further evidence for the utility of the meta-theory, and prepare the ground for combining our instantiation with other, already existing instantiations.
Comments: 24 pages. This is the full version of the paper An Abstract Contract Theory for Programs with Procedures, published in Proceedings of the 24th International Conference on Fundamental Approaches to Software Engineering (FASE 2021), which includes the proofs of all theorems and additional examples. The conference version should always be cited
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
ACM classes: D.2.4; F.3.1; F.3.2
Cite as: arXiv:2101.06087 [cs.LO]
  (or arXiv:2101.06087v2 [cs.LO] for this version)

Submission history

From: Christian Lidström [view email]
[v1] Fri, 15 Jan 2021 13:02:57 GMT (34kb)
[v2] Fri, 11 Jun 2021 08:16:29 GMT (45kb)

Link back to: arXiv, form interface, contact.