next up previous contents
Next: Version 1.0 Up: Release Notes Previous: Version 2.0 (April 1995)   Contents

Version 1.6

In this version in all kinds of transitive relations are dealt with in a uniform way by chaining inferences.

There is still no full implementation for inheriting constraints.

Subdirectories hoare and bledsoe of saturate/examples exercise ordering relations. In hoare you find lemmas that occur in the verification of quicksort and binary search algorithms. The directory bledsoe contains examples from various papers by Bledsoe, including the intermediate value theorem and the challenge problems stated in a JAR paper from 1990.



Harald Ganzinger 2002-12-04

Imprint | Data Protection