• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Teaching the Construction of Correct Programs Using Invariant Based Programming

Ralph-Johan Back, Johannes Eriksson, Linda Mannila, Teaching the Construction of Correct Programs Using Invariant Based Programming. In: Proceedings of the 3rd South-East European Workshop on Formal Methods, 2007.

Abstract:

In most computer science curricula, formal reasoning about program correctness is taught
separately from practical programming, and is thus by most students considered a purely
theoretical activity. It has been a challenge to convince students of the practical applicability of
formal methods. We present here an effort to apply Invariant Based Programming (IBP), a visual
and practical program construction and verification methodology, in an introductory formal
methods course as part of a pilot study at ˚ Abo Akademi University. The course introduces a
minimum of notational overhead, and allows the student to reason about correctness using
mathematical concepts with which they are already familiar (such as set theory). We have used a
programming environment with theorem prover support (SOCOS) to increase student confidence
in the correctness of the program components that they construct. We evaluate the course using
a mixed method approach, and provide data which show that IBP is well suited for teaching
introductory formal methods.

Files:

Full publication in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpBaErMa07a,
  title = {Teaching the Construction of Correct Programs Using Invariant Based Programming},
  booktitle = {Proceedings of the 3rd South-East European Workshop on Formal Methods},
  author = {Back, Ralph-Johan and Eriksson, Johannes and Mannila, Linda},
  year = {2007},
}

Belongs to TUCS Research Unit(s): Learning and Reasoning Lab

Edit publication