Generic weakest precondition semantics from monads enriched with order

作     者：Hasuo, Ichiro 

作者机构：Univ Tokyo Dept Comp Sci Tokyo 1138656 Japan 

出 版 物：《THEORETICAL COMPUTER SCIENCE》 (理论计算机科学)

年 卷 期：2015年第604卷

页      面：2-29页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：JSPS Aihara Innovative Mathematical Modelling Project, FIRST Program, JSPS/CSTP Grants-in-Aid for Scientific Research [15KT0012, 15K11984, 24680001] Funding Source: KAKEN 

主　　题：Program verification Program logic Precondition calculus Nondeterminism Game Effect Algebra Coalgebra Categorical model Monad 

摘      要：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 alternating branching like in games and in probabilistic systems with nondeterministic environments is modularly modeled by a monad on the Eilenberg-Moore category of another. (C) 2015 Elsevier B.V. All rights reserved.