A Hoare Logic for the State Monad Proof Pearl

被引：0

作者：

Swierstra, Wouter ^{[1
]}

机构：

[1] Chalmers Univ Technol, Gothenburg, Sweden

来源：

THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS | 2009年 / 5674卷

关键词：

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This pearl examines how to verify functional programs written using the state monad. It uses Coq's Program framework to provide strong specifications for the standard operations that the state monad supports; such as return and bind. By exploiting the monadic structure of such programs during the verification process, it becomes easier to prove that they satisfy their specification.

引用

页码：440 / 451

页数：12

共 50 条

[1] Monad-independent Hoare logic in HASCASL
Schröder, L
Mossakowski, T
[J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2003, 2621 : 261 - 277
[2] A Proof System for HRML with Extended Hoare Logic
Chen, Ningning
Zhu, Huibiao
Fang, Huixing
[J]. 2021 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2021), 2021, : 31 - 38
[3] Proof of correctness of C++ program by HOARE logic
Wang, Caifen
[J]. Lanzhou Daxue Xuebao/Journal of Lanzhou University, 2000, 36 (01): : 44 - 47
[4] SOUNDNESS OF HOARE LOGIC - AN AUTOMATED PROOF USING LCF
SOKOLOWSKI, S
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1987, 9 (01): : 101 - 120
[5] A Proof Tree Builder for Sequent Calculus and Hoare Logic
Korkut, Joomy
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2023, (375): : 54 - 62
[6] A LANGUAGE INDEPENDENT PROOF OF THE SOUNDNESS AND COMPLETENESS OF GENERALIZED HOARE LOGIC
COUSOT, P
COUSOT, R
[J]. INFORMATION AND COMPUTATION, 1989, 80 (02) : 165 - 191
[7] The proof monad
Kirchner, Florent
Munoz, Cesar
[J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2010, 79 (3-5): : 264 - 277
[8] SOUNDNESS OF HOARE'S LOGIC: AN AUTOMATED PROOF USING LCF.
Sokolowski, Stefan
[J]. ACM Transactions on Programming Languages and Systems, 1987, 9 (01): : 100 - 120
[9] Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
Mizutani, Shinnosuke
Nishida, Naoki
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (265): : 35 - 51
[10] Interfacing hoare logic and type systems for Foundational Proof-Carrying Code
Hamid, NA
Shao, Z
[J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2004, 3223 : 118 - 135

← 1 2 3 4 5 →