Please use this identifier to cite or link to this item: https://repositorio.escuelaing.edu.co/handle/001/301
Title: Executable calculational expessions
Authors: Cháves Alonso, Fransisco José
Rocha Niño, Hernán Camilo
Keywords: Haskell
Calculational logic
Formal Specification
Formal Methods
Dijkstra and Scholtem Style
Big operators
Estilo Dijkstra y Scholtem
Operatorias
Lógica Calculatoria
Issue Date: 2015
Abstract: 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 manuscript 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 also included.
URI: http://repositorio.escuelaing.edu.co/handle/001/301
Appears in Collections:IF - Working papers

Files in This Item:
File Description SizeFormat 
IF-Reporte Tecnico-79455788.pdfPDF475.49 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.