Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Theorem Prover Support for Pre...

Theorem Prover Support for Precondition and Correctness Calculation

Orieta Celiku, Joakim von Wright, Theorem Prover Support for Precondition and Correctness Calculation. TUCS Technical Reports 449, Turku Centre for Computer Science, 2002.

Abstract:

Tools for automatically extracting the conditions for which a program
is correct with respect to a precondition and postcondition can make proving
program correctness easier. We build a HOL-based tool that uses weakest
preconditions to prove correctness theorems with the verification conditions
as assumptions. The programming language includes loops, (recursive)
procedures, and also both demonic and angelic nondeterminism, which can
be used to model interaction. Program variables can be of arbitrary types.
Programs with procedures are handled modularly, and proved facts about
individual procedures are stored in a database available to all programs. We
also discuss two new rules for calculating loop preconditions and recursion
correctness while taking into consideration specification variables.

Files:

Abstract in PDF-format

BibTeX entry:

@TECHREPORT{tCevo02a,
  title = {Theorem Prover Support for Precondition and Correctness Calculation},
  author = {Celiku, Orieta and Wright, Joakim von},
  number = {449},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2002},
}

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

Edit publication