Princeton University
Computer Science Department

Computer Science 598A
Automated Theorem Proving

Andrew Appel

Assignment 8
Spring 2003

General Information | Schedule | Assignments | Announcements
Assignment 8
Take this implementation of Hoare logic and put it in a subdirectory hoare of your as5 logic directory.

In minsum.elf is a program (described in Huth and Ryan) that computes the minimum subsequence sum of an array a: 

minsum = ( k gets two ; 
           t gets (a @ one) ;
           s gets (a @ one) ;
           while (neq k (plus n one))
            (t gets (min @ plus t (a @ k) @ (a @ k)) ;
             s gets (min @ s @ t) ;
             k gets plus k one)).
Your task is to prove the theorem
pf_minsum : pf (triple true minsum (post1 and post2)) = ...

You can find some substitutions and lemmas to get you started in minsol.elf.