TY - GEN
T1 - Executable calculational specifications
AU - Chaves, Francisco
AU - Rocha, Camilo
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/11/20
Y1 - 2015/11/20
N2 - The calculational style of E. W. Dijkstra and C. S. Scholten is a semi-formal style for the development, both in terms of verification and derivation, of correct programs. This calculational style heavily relies on the symbolic manipulation of expressions involving, for instance, arithmetic, quantifiers, and collections. This paper presents Calculational, an executable specification language for a broad class of calculational expressions in the style of Dijkstra & Scholten. The Calculational tool offers support for executable specifications, including: (i) quantifier expressions such as summation and universal/existential quantification, and (ii) data types such as lists, sets, and bags (i.e., multisets). The current implementation of Calculational is executable in the Haskell programming language, offering support also for higher order computation and pattern matching. This implementation is available for download as open source code and as a Haskell library too (which can be embedded in other programming languages). The main features of Calculational, some examples of its use-including the formal processing and querying of relational data-, and details of its implementation are included in this paper.
AB - The calculational style of E. W. Dijkstra and C. S. Scholten is a semi-formal style for the development, both in terms of verification and derivation, of correct programs. This calculational style heavily relies on the symbolic manipulation of expressions involving, for instance, arithmetic, quantifiers, and collections. This paper presents Calculational, an executable specification language for a broad class of calculational expressions in the style of Dijkstra & Scholten. The Calculational tool offers support for executable specifications, including: (i) quantifier expressions such as summation and universal/existential quantification, and (ii) data types such as lists, sets, and bags (i.e., multisets). The current implementation of Calculational is executable in the Haskell programming language, offering support also for higher order computation and pattern matching. This implementation is available for download as open source code and as a Haskell library too (which can be embedded in other programming languages). The main features of Calculational, some examples of its use-including the formal processing and querying of relational data-, and details of its implementation are included in this paper.
UR - http://www.scopus.com/inward/record.url?scp=84963861024&partnerID=8YFLogxK
U2 - 10.1109/ColumbianCC.2015.7333398
DO - 10.1109/ColumbianCC.2015.7333398
M3 - Conference contribution
AN - SCOPUS:84963861024
T3 - 2015 10th Colombian Computing Conference, 10CCC 2015
SP - 1
EP - 8
BT - 2015 10th Colombian Computing Conference, 10CCC 2015
A2 - Gonzalez, Oscar
A2 - Sanchez, Mario
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 10th Colombian Computing Conference, 10CCC 2015
Y2 - 21 September 2015 through 25 September 2015
ER -