WP4PI: a proof system based on the weakest preconditions for the applied -calculus
Decai Jiao, David A. Sinclair · China-Ireland International Conference on Information and Communications Technologies (CIICT 2007) · 2007
The π-calculus provides a simple but powerful formal basis for specification and verification of parallel and distributed systems with evolving structures. Applied π-calculus is a general extension of the π-calculus with value passing, primitive functions and equations among terms. In this paper, we present WP4PI, a proof system based on the weakest preconditions for the applied π-calculus. An algorithm is developed to compute the fixpoint of the weakest precondition for a recursive process and a balanced binary tree structure is used to deal with the complexity introduced by conditional construct of the applied π-calculus. Primitive functions in the applied π-calculus are handled by equipping the proof system with an extensible equation sub-system. Based on the weakest preconditions and Hoare's logic, WP4PI is a target-oriented proof system and captures the term substitution property of the applied π-calculus.