Hoarescope helps to prove partial correctness
assertions of AL programs over natural numbers
using Hoare logic (Hoare calculus). It can be used
as an aid for teaching and learning this aspect of
theoretical computer science at the undergraduate
level. Hoarescope performs inferences as far as
possible, usually leaving only a few terms for the
user to prove. The resulting proof tree is
exported to LaTeX for easy inclusion in your own
documents.
