Specification Verification of Hoare's Quicksort Algorithm in CafeOBJ

• Kokichi Futatsugi

================================
Title:
Specification Verification of Hoare's Quicksort Algorithm
in CafeOBJ

by Kokichi Futatsugi (AIST/JAIST/NII)

Abstract:

Sorting is modeled as an operation on sequences of elements with an
order relation, and Hoare's quicksort algorithm is specified as a
transition system in CafeOBJ specification/verification system.  The
correctness of the sort algorithm is specified as a leads-to property
of the transition system, and a proof score is developed to prove the
property.

The proof score makes use of built-in search predicates extensively to
prove basic leads-to properties, which are formulated with transition
rules as inference rules for proving the target leads-to property
inductively.  The proof score developed has a potential to make proofs
of a wide variety of leads-to properties possible.
===================================