Substructural logic and partial correctness

We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and trace models. As a corollary we obtain a complete sequent calculus for inclusion and equivalence of regular expressions. Categories and Subject Descriptors: D.2.2 [Software Engineering]: Tools and Techniques— structured programming; D.2.4 [Software Engineering]: Program Verification—correctnes