Verification of SequenceL programs using Mizar

Date

2010-08

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Purely functional language programs are claimed to lend themselves more easily to their proof of correctness. SequenceL, exclusively designed at Texas Tech University, is a strict functional language. There are some proof-assistants used in verification of functional language programs. In this research, we used one of the available proof assistants called Mizar to prove correctness of SequenceL programs. Mizar is based on Tarski-Grothendieck set theory formulated in a first-order language. The Mizar language is human readable compared to other formal systems. It also has some other desirable features for our purposes. The result of this research is a Mizar file that describes a semantics of SequenceL and the framework in which properties of SequenceL programs can be proved. Some examples such as factorial and Euclidian greatest common divisor are given in the Mizar file. Also, a reasonably sized library of proven statements is provided intended to shorten the proofs of properties of SequenceL programs.

Description

Citation