TY - JOUR
T1 - Compositional specification of commercial contracts
AU - Andersen, Jesper
AU - Elsborg, Ebbe
AU - Henglein, Fritz
AU - Simonsen, Jakob Grue
AU - Stefansen, Christian Oskar Erik
PY - 2006
Y1 - 2006
N2 - We present a declarative language for compositional specification of contracts governing the exchange of resources. It extends Eber and Peyton Jones’s declarative language for specifying financial contracts (Jones et al. in The Fun of Programming. 2003) to the exchange of money, goods and services amongst multiple parties and complements McCarthy’s Resources, Events and Agents (REA) accounting model (McCarthy in Account Rev. LVII(3), 554–578, 1982) with a view- independent formal contract model that supports definition of user-defined contracts, automatic monitoring under execution and user-definable analysis of their state before, during and after execution. We provide several realistic examples of commercial contracts and their analyses. A variety of (real) contracts can be expressed in such a fashion as to support their integration, management and analysis in an operational environment that registers events. The language design is driven by both domain considerations and semantic language design methods: a contract denotes a set of traces of events, each of which is an alternative way of concluding the contract successfully, which gives rise to a CSP-style (Brooker et al. in J.ACM 31(3), 560–599, 1984; Hoare in Communicating Sequential Processes, 1985) denotational semantics. The denotational semantics drives the development of a sound and complete small-step operational semantics, where a partially executed contract is represented as a (full) contract that represents the remaining contractual commitments. This operational semantics is then systematically refined in two stages to an instrumented operational semantics that reflects the bookkeeping practice of identifying the specific contractual commitment a particular event matches at the time the event occurs, as opposed to delaying this matching until the contract is concluded.
AB - We present a declarative language for compositional specification of contracts governing the exchange of resources. It extends Eber and Peyton Jones’s declarative language for specifying financial contracts (Jones et al. in The Fun of Programming. 2003) to the exchange of money, goods and services amongst multiple parties and complements McCarthy’s Resources, Events and Agents (REA) accounting model (McCarthy in Account Rev. LVII(3), 554–578, 1982) with a view- independent formal contract model that supports definition of user-defined contracts, automatic monitoring under execution and user-definable analysis of their state before, during and after execution. We provide several realistic examples of commercial contracts and their analyses. A variety of (real) contracts can be expressed in such a fashion as to support their integration, management and analysis in an operational environment that registers events. The language design is driven by both domain considerations and semantic language design methods: a contract denotes a set of traces of events, each of which is an alternative way of concluding the contract successfully, which gives rise to a CSP-style (Brooker et al. in J.ACM 31(3), 560–599, 1984; Hoare in Communicating Sequential Processes, 1985) denotational semantics. The denotational semantics drives the development of a sound and complete small-step operational semantics, where a partially executed contract is represented as a (full) contract that represents the remaining contractual commitments. This operational semantics is then systematically refined in two stages to an instrumented operational semantics that reflects the bookkeeping practice of identifying the specific contractual commitment a particular event matches at the time the event occurs, as opposed to delaying this matching until the contract is concluded.
KW - Faculty of Science
U2 - 10.1007/s10009-006-0010-1
DO - 10.1007/s10009-006-0010-1
M3 - Journal article
SN - 1433-2779
SP - 485
EP - 516
JO - International Journal on Software Tools for Technology Transfer
JF - International Journal on Software Tools for Technology Transfer
ER -