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. (Source: http://freecode.com/)