Please use this identifier to cite or link to this item:
Exportar a Bibtex Exportar a RIS Exportar a Excel Buscar en google Schoolar Buscar en microsoft academic
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
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.
Appears in Collections:IF - Working papers

Files in This Item:
File Description SizeFormat 
IF-Reporte Tecnico-79455788.pdfPDF475.49 kBAdobe PDFThumbnail
Show full item record

Page view(s)

checked on Nov 9, 2017


checked on Nov 9, 2017

Google ScholarTM


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