João F. Ferreira (约恩)*

PhD Student on Algorithmic Problem Solving

[ CiteULike link ]
Authors

J. Visser, J. N. Oliveira, L. S. Barbosa, João F. Ferreira, and A. Mendes

Downloads
  • Paper: PDF
  • Slides of the talk given at the Overture Workshop: PDF
Status

Published in Nico Plat and Peter Gorm Larsen, editors, Overture Workshop (co-located with FM'05), University of Newcastle upon Tyne, UK, July, 2005.

Abstract

We have experimented with modeling some of the key concepts of the VDM specification language inside the functional programming language Haskell. For instance, VDM’s sets and maps are directly available as data types defined in standard libraries; we merely needed to define some additional functions to make the match complete. A bigger challenge is posed by VDM’s data type invariants, and pre- and post-conditions. For these we resorted to Haskell’s constructor class mechanism, and its support for monads. This allows us to switch between different modes of evaluation (e.g. with or without property checking) by simply coercing user defined functions and operations to different specific types.

Keywords

Camila, Formal Methods, Formal Specification, Datatype Invariants, Pre-Conditions, Post-Conditions, Haskell

Bibtex entry
@inproceedings{jff*05:camila,
    author = {Visser, Joost   and Oliveira, Jos\'{e}  N.  and Barbosa, 
              Luis  S.  and Ferreira, Jo\~{a}o  F.  and Mendes, Alexandra  S. },
    booktitle = {First Overture Workshop},
    title = {Camila Revival: VDM meets Haskell},
    year = {2005},
    url = {http://joaoff.com/publications/2005/camila},
    citeulike-article-id = {873504}
}
History
  • 2005 — published and presented at Overture Workshop, Newcastle