Waldek, >The real question is how to do this. Several years ago >my student did "by hand" a proof in Hoare logic of a simple 20 >line long program. The proof is 20 pages long. The proof >is rather detailed, but he consided some facts as known >and some readers probably would ask questions demanding >more details.
Was this proof published anywhere? Do you have a URL? Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer