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

Reply via email to