Name
Abstract | ||
|---|---|---|
Behavioral software contracts have become a popular mechanism for specifying and ensuring logical claims about a program's flow of values. While contracts for first-order functions come with a natural interpretation and are well understood, the various incarnations of higher-order contracts adopt, implicitly or explicitly, different views concerning the meaning of contract satisfaction. In this article, we define various notions of contract satisfaction in terms of observational equivalence and compare them with each other and notions in the literature. Specifically, we introduce a small model language with higher-order contracts and use it to formalize different notions of contract satisfaction. Each of them demands that the contract parties satisfy certain observational equivalences. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/2039346.2039348 | ACM Trans. Program. Lang. Syst. |
Keywords | Field | DocType |
different view,contract party,different notion,various incarnation,observational equivalence,various notion,higher-order world,certain observational equivalence,behavioral software contract,higher-order contract,contract satisfaction,satisfiability,modeling language,first order,higher order | Observational study,Observational equivalence,Computer science,Algorithm,Theoretical computer science,Software,Management science | Journal |
Volume | Issue | ISSN |
33 | 5 | 0164-0925 |
Citations | PageRank | References |
18 | 0.77 | 17 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christos Dimoulas | 1 | 96 | 6.44 |
| Matthias Felleisen | 2 | 3001 | 272.57 |