Algebraic specification and formal methods for program development: what are the real problems?

Andrzej Tarlecki, Donald Sannella

Research output: Chapter in Book/Report/Conference proceedingChapter


The long-term goal of work on algebraic specification is formal development of correct programs from specifications via verified-correct refinement steps. Define a real problem to be an unsolved problem which lies on (or near) the path betwen the current state of the art and this ultimate goal. Long-term progress depends on solving these problems, so it seems worthwhile to attack the real problems before worrying about other issues. It is perhaps surprising that there is little agreement concerning what these problems are, at least if one takes the problems being tackled as an indication of what various researchers think the real problems are. Some sort of consensus seems desirable to promote effective joint progress towards our common goal. We list some (not all) of what we think are the real problems. In an attempt to spark controversy, some things which we think are not real problems are also listed. Neither of these lists is exhaustive.
Original languageEnglish
Title of host publicationCurrent Trends In Theoretical Computer Science
PublisherWorld Scientific Press
Number of pages6
ISBN (Print)978-981-02-1462-3
Publication statusPublished - 1993

Publication series

NameWorld Scientific Series in Computer Science
VolumeVolume 40


Dive into the research topics of 'Algebraic specification and formal methods for program development: what are the real problems?'. Together they form a unique fingerprint.

Cite this