Automatic Pre- and Postconditions for Partial Differential Equations

Based on a simple automata-theoretic and algebraic framework, we study equational reasoning for Initial Value Problems (IVPs) of polynomial Partial Differential Equations (PDEs). In order to represent IVPs in their full generality, we introduce stratified systems, where function definitions can be decomposed into distinct subsystems, focusing on different subsets of independent variables. Under a certain coherence condition, for such stratified systems we prove existence and uniqueness of formal power series solutions, which conservatively extend the classical analytic ones. We then give a-in a precise sense, complete-algorithm to compute weakest preconditions and strongest postconditions for such systems. To some extent, this result reduces equational reasoning on PDE initial value (and boundary) problems to algebraic reasoning. We illustrate some experiments conducted with a proof-of-concept implementation of the method.