Hoare type theory, polymorphism and separation. (English) Zbl 1155.68354
Summary: We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and nontermination. We propose Hoare Type Theory (HTT), which incorporates Hoare-style specifications into types, making it possible to statically track and enforce correct use of side effects.
The main feature of HTT is the Hoare type {P}x:A{Q} specifying computations with precondition P and postcondition Q that return a result of type A. Hoare types can be nested, combined with other types, and abstracted, leading to a smooth integration with higher-order functions and type polymorphism.
We further show that in the presence of type polymorphism, it becomes possible to interpret the Hoare types in the “small footprint” manner, as advocated by separation logic, whereby specifications tightly describe the state required by the computation.
We establish that HTT is sound and compositional, in the sense that separate verifications of individual program components suffice to ensure the correctness of the composite program.
The main feature of HTT is the Hoare type {P}x:A{Q} specifying computations with precondition P and postcondition Q that return a result of type A. Hoare types can be nested, combined with other types, and abstracted, leading to a smooth integration with higher-order functions and type polymorphism.
We further show that in the presence of type polymorphism, it becomes possible to interpret the Hoare types in the “small footprint” manner, as advocated by separation logic, whereby specifications tightly describe the state required by the computation.
We establish that HTT is sound and compositional, in the sense that separate verifications of individual program components suffice to ensure the correctness of the composite program.
MSC:
| 68N18 | Functional programming and lambda calculus |
Keywords:
Hoare-style specificationsReferences:
| [1] | DOI: 10.1145/570886.570888 · doi:10.1145/570886.570888 |
| [2] | DOI: 10.1145/964001.964020 · Zbl 1325.68041 · doi:10.1145/964001.964020 |
| [3] | DOI: 10.1145/1086365.1086400 · Zbl 1302.68095 · doi:10.1145/1086365.1086400 |
| [4] | Leavens, Behavioral Specifications of Businesses and Systems pp 175– (1999) · doi:10.1007/978-1-4615-5229-1_12 |
| [5] | Watkins, Types for Proofs and Programs pp 355– (2004) · doi:10.1007/978-3-540-24849-1_23 |
| [6] | Berger, International Conference on Functional Programming ICFP 5 pp 280– (2005) |
| [7] | Krishnaswami, Workshop on Semantics, Program Analysis and Computing Environments for Memory Management SPAC’06 pp 73– (2006) |
| [8] | DOI: 10.1145/289423.289429 · Zbl 1370.68050 · doi:10.1145/289423.289429 |
| [9] | Barnes, High Integrity Software: The SPARK Approach to Safety and Security (2003) |
| [10] | Jim, USENIX Annual Technical Conference, USENIX’02 pp 275– (2002) |
| [11] | Tan, International Conference on Verification, Model Checking and Abstract Interpretation VMCAI’06 pp 80– (2006) |
| [12] | DOI: 10.1145/289423.289451 · Zbl 1369.68085 · doi:10.1145/289423.289451 |
| [13] | Howard, Essays on Combinatory Logic, Lambda Calculus and Formalism pp 479– (1980) |
| [14] | The HOL System: Description (1991) |
| [15] | Amtoft, Symposium on Principles of Programming Languages POPL 06 pp 91– (2006) |
| [16] | Honda, Symposium on Logic in Computer Science LICS’05 pp 270– (2005) |
| [17] | Smith, European Symposium on Programming ESOP’00 pp 366– (2000) |
| [18] | DOI: 10.1109/LICS.2001.932506 · doi:10.1109/LICS.2001.932506 |
| [19] | Sheard, International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA’04 pp 116– (2004) |
| [20] | DOI: 10.1145/1086365.1086376 · Zbl 1302.68048 · doi:10.1145/1086365.1086376 |
| [21] | DOI: 10.1145/363235.363259 · Zbl 0179.23105 · doi:10.1145/363235.363259 |
| [22] | DOI: 10.1145/1053468.1053469 · doi:10.1145/1053468.1053469 |
| [23] | Abadi, Verification: Theory and Practice pp 11– (2004) |
| [24] | DOI: 10.1145/1065944.1065952 · doi:10.1145/1065944.1065952 |
| [25] | DOI: 10.1109/LICS.2002.1029817 · doi:10.1109/LICS.2002.1029817 |
| [26] | Reus, International Workshop on Computer Science Logic CSL’06 (2006) |
| [27] | DOI: 10.1145/567752.567769 · doi:10.1145/567752.567769 |
| [28] | Girard, Proofs and Types (1989) |
| [29] | DOI: 10.1145/345099.345100 · doi:10.1145/345099.345100 |
| [30] | DOI: 10.1145/165180.165214 · doi:10.1145/165180.165214 |
| [31] | DOI: 10.1017/S0960129501003322 · Zbl 0997.03020 · doi:10.1017/S0960129501003322 |
| [32] | DOI: 10.1007/BFb0014052 · doi:10.1007/BFb0014052 |
| [33] | DOI: 10.1145/158511.158524 · doi:10.1145/158511.158524 |
| [34] | Fluet, European Symposium on Programming ESOP’06 pp 7– (2006) |
| [35] | Peyton, Haskell 98 Language and Libraries: The Revised Report (2003) · Zbl 1067.68041 |
| [36] | Flanagan, Symposium on Principles of Programming Languages POPL’06 pp 245– (2006) |
| [37] | Paulson, International Conference in Computer Logic, COLOG’88 pp 246– (1990) |
| [38] | Feng, European Symposium on Programming ESOP’07 pp 173– (2007) |
| [39] | DOI: 10.1145/964001.964024 · Zbl 1325.68069 · doi:10.1145/964001.964024 |
| [40] | DOI: 10.1109/52.976940 · doi:10.1109/52.976940 |
| [41] | O’Hearn, International Workshop on Computer Science Logic CSL’01 pp 1– (2001) |
| [42] | DOI: 10.1016/j.jlap.2005.07.001 · Zbl 1080.68014 · doi:10.1016/j.jlap.2005.07.001 |
| [43] | DOI: 10.1145/358728.358748 · Zbl 0495.68018 · doi:10.1145/358728.358748 |
| [44] | DOI: 10.1007/BF01211308 · Zbl 0808.03044 · doi:10.1007/BF01211308 |
| [45] | DOI: 10.1145/263699.263712 · doi:10.1145/263699.263712 |
| [46] | Nanevski, European Symposium on Programming ESOP’07 pp 189– (2007) |
| [47] | DOI: 10.1145/360933.360975 · Zbl 0308.68017 · doi:10.1145/360933.360975 |
| [48] | Morrisett, International Conference on Typed Lambda Calculus and Applications TLCA’05 pp 293– (2005) · doi:10.1007/11417170_22 |
| [49] | DOI: 10.1137/0207005 · Zbl 0374.68009 · doi:10.1137/0207005 |
| [50] | DOI: 10.1016/0890-5401(91)90052-4 · Zbl 0723.68073 · doi:10.1016/0890-5401(91)90052-4 |
| [51] | Condit, European Symposium on Programming ESOP’07 (2007) |
| [52] | Moggi, Symposium on Logic in Computer Science LICS’89 pp 14– (1989) |
| [53] | DOI: 10.1016/j.entcs.2006.04.010 · doi:10.1016/j.entcs.2006.04.010 |
| [54] | McCarthy, Congress of the International Federation for Information Processing, IFIP’62 pp 21– (1962) |
| [55] | DOI: 10.2307/2266170 · Zbl 0023.28901 · doi:10.2307/2266170 |
| [56] | DOI: 10.1017/S0956796803004829 · Zbl 1069.68539 · doi:10.1017/S0956796803004829 |
| [57] | DOI: 10.1145/1086365.1086375 · Zbl 1302.68241 · doi:10.1145/1086365.1086375 |
| [58] | DOI: 10.1145/512760.512774 · doi:10.1145/512760.512774 |
| [59] | Martin-Löf, Nordic J. Philosophic. Logic 1 pp 11– (1996) |
| [60] | DOI: 10.1007/s10009-004-0167-4 · doi:10.1007/s10009-004-0167-4 |
| [61] | DOI: 10.1145/944705.944725 · Zbl 1315.68055 · doi:10.1145/944705.944725 |
| [62] | DOI: 10.1109/LICS.2005.47 · doi:10.1109/LICS.2005.47 |
| [63] | Luo, Computation and Reasoning: A Type Theory for Computer Science (1994) · Zbl 0823.68101 |
| [64] | Zhu, Practical Aspects of Declarative Languages PADL’05 pp 83– (2005) · doi:10.1007/978-3-540-30557-6_8 |
| [65] | DOI: 10.1145/292540.292560 · doi:10.1145/292540.292560 |
| [66] | DOI: 10.1145/277650.277732 · doi:10.1145/277650.277732 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
