Holistic specifications for robust programs
File(s)
Author(s)
Drossopoulou, Sophia
Noble, James
MacKay, Julian
Eisenbach, Susan
Type
Conference Paper
Abstract
Functional specifications describe what program components can do: the sufficient conditions to invoke components' operations. They allow us to reason about the use of components in a closed world setting, where
components interact with known client code, and where the client code must establish the appropriate pre-conditions before calling into a component.
Sufficient conditions are not enough to reason about the use of components in an \emph{open world} setting, where components interact with external code, possibly of unknown provenance, and where components may evolve over time.
In this open world setting, we must also consider the possible external code. \emph{necessary} conditions, i.e, what are the conditions without which an effect will not happen.
In this paper we propose the Chainmail specification language for writing {holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for \Chainmail, and discuss several examples. The core of \Chainmail has been mechanised in the Coq proof assistant.
components interact with known client code, and where the client code must establish the appropriate pre-conditions before calling into a component.
Sufficient conditions are not enough to reason about the use of components in an \emph{open world} setting, where components interact with external code, possibly of unknown provenance, and where components may evolve over time.
In this open world setting, we must also consider the possible external code. \emph{necessary} conditions, i.e, what are the conditions without which an effect will not happen.
In this paper we propose the Chainmail specification language for writing {holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for \Chainmail, and discuss several examples. The core of \Chainmail has been mechanised in the Coq proof assistant.
Editor(s)
Wehrheim, Heike
Cabot, Jodi
Date Issued
2020-04-17
Date Acceptance
2020-02-22
Citation
Lecture Notes in Computer Science, 2020, 12076
ISSN
0302-9743
Publisher
Springer Verlag
Journal / Book Title
Lecture Notes in Computer Science
Volume
12076
Copyright Statement
© The Author(s) 2020. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
Identifier
https://wp.doc.ic.ac.uk/sd/
Source
International Conference on Fundamental Approaches to Software Engineering
Subjects
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2020-04-25
Finish Date
2020-04-30
Coverage Spatial
Dublin, Ireland
Date Publish Online
2020-04-17