License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICLP.2011.95
URN: urn:nbn:de:0030-drops-31810
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3181/
Go to the corresponding LIPIcs Volume Portal

Herranz, Ángel ; Mariño, Julio

Synthesis of Logic Programs from Object-Oriented Formal Specifications

pdf-format:
24.pdf (0.5 MB)

Abstract

Early validation of requirements is crucial for the rigorous development of software. Without it, even the most formal of the methodologies will produce the wrong outcome. One successful approach, popularised by some of the so-called lightweight formal methods, consists in generating (finite, small) models of the specifications. Another possibility is to build a running prototype from those specifications. In this paper we show how to obtain executable prototypes from formal specifications written in an object oriented notation by translating them into logic programs. This has some advantages over other lightweight methodologies. For instance, we recover the possibility of dealing with recursive data types as specifications that use them often lack finite models.

BibTeX - Entry

@InProceedings{herranz_et_al:LIPIcs:2011:3181,
  author =	{Ángel Herranz and Julio Mari{\~n}o},
  title =	{{Synthesis of Logic Programs from Object-Oriented Formal Specifications}},
  booktitle =	{Technical Communications of the 27th International Conference on Logic Programming (ICLP'11) },
  pages =	{95--105},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-31-6},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{11},
  editor =	{John P. Gallagher and Michael Gelfond},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3181},
  URN =		{urn:nbn:de:0030-drops-31810},
  doi =		{10.4230/LIPIcs.ICLP.2011.95},
  annote =	{Keywords: Formal Methods, Logic Program Synthesis, Object-Oriented, Executable Specifications, Correct-by-Construction}
}

Keywords: Formal Methods, Logic Program Synthesis, Object-Oriented, Executable Specifications, Correct-by-Construction
Collection: Technical Communications of the 27th International Conference on Logic Programming (ICLP'11)
Issue Date: 2011
Date of publication: 27.06.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI