Prev Up Next
Go backward to Applying Larch/C++ to the STL
Gary Leavens

Go up to Specification and Verification
Go forward to Language Independent Container Specification
Alexandre Zamulin


Mizar Verification of Generic Algebraic Algorithms
Christoph Schwarzweller

We propose the Mizar system as a theorem prover capable of verifying generic algebraic algorithms on an appropriate abstract level. The main advantage of the Mizar theorem prover is its special input language that enables textbook-style presentation of proofs, hence proofs in the language of algebra. Using Mizar we were able to give a rigorous machine-assisted correctness proof of a generic version of Brown/Henrici arithmetic in the field of quotients over arbitrary gcd domains. In this talk we give a short introduction into the Mizar language and show how to use the system to verify generic algebraic algorithms. We also deal with proof documentation based on literate programming, claiming that even complex proofs can be presented so that they stay readable and understandable.


 

Prev Up Next