[isabelle] IMP Program


I need an interesting IMP program  to prove it correct using  Hoare logic  in Isabelle.
And this program must be interesting and non so complicated  because i need it for my essay and i don’t have so much i have around  one month left .
If any one can provide with an idea or something i will be grateful 

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.