A characterization of weakest preconditions
作者：
Highlights：
•
摘要
If S is a set of states, a function f:2S → 2S is the “weakest precondition” map of somemechanism of bounded nondeterminacy if and only if it is strict, preserves binary intersections, and is continuous over directed sets. If S is countable, the continuity condition may be weakened to continuity over ω-chains.
论文关键词：
论文评审过程：Received 11 June 1976, Revised 24 November 1976, Available online 27 December 2007.
论文官网地址：https://doi.org/10.1016/S0022-0000(77)80006-8
