Abstract : We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs’ recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: (1) different notions of modality (such as “may” vs. “must”) are captured by Eilenberg-Moore algebras; (2) nested branching—like in games and in probabilistic systems with nondeterministic environments—is modularly modeled by a monad on the Eilenberg-Moore category of another.
https://hal.inria.fr/hal-01408750 Contributor : Hal IfipConnect in order to contact the contributor Submitted on : Monday, December 5, 2016 - 1:21:15 PM Last modification on : Monday, May 17, 2021 - 12:00:04 PM Long-term archiving on: : Monday, March 20, 2017 - 9:25:00 PM
Ichiro Hasuo. Generic Weakest Precondition Semantics from Monads Enriched with Order. 12th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2014), Apr 2014, Grenoble, France. pp.10-32, ⟨10.1007/978-3-662-44124-4_2⟩. ⟨hal-01408750⟩