A General Completeness Result in Refinement

Yoshiki Kinoshita, John Power

Research output: Chapter in Book/Report/Conference proceedingChapter

3 Citations (Scopus)

Abstract

In a paper in 1986, Hoare, He and Sanders proposed a formulation of refinement for a system equivalent to the ν-calculus using a relation based semantics. To give a proof method to show that one program is a refinement of another, they introduced downward simulation and upward simulation, but the proof method based upon either of them is not complete with respect to their notion of refinement, so they claimed “joint” completeness based upon both notions of simulation with respect to their notion of refinement.

We give a new definition of refinement in terms of structure respecting lax transformations, and show that the proof method based upon downward simulation is complete with respect to this notion of refinement. Although our theory works for the ν-calculus, we present the result for the μ-calculus to make the presentation simpler. We use results in enriched category theory to show this, and the central notion here is that of algebraic structure on locally ordered categories, not on sets. Our definition of refinement is neither a restriction nor a generalisation of Hoare, He and Sanders’ definition, but we include all their important examples.

Original languageEnglish
Title of host publicationRecent Trends in Algebraic Development Techniques
Place of PublicationHeidelberg
PublisherSpringer
Pages201-218
Number of pages18
Volume1827
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Fingerprint

Completeness
Refinement
Calculus
Simulation
Enriched Category
Ordered Categories
μ-calculus
Category Theory
Algebraic Structure
Restriction
Formulation

Cite this

Kinoshita, Y., & Power, J. (2000). A General Completeness Result in Refinement. In Recent Trends in Algebraic Development Techniques (Vol. 1827, pp. 201-218). (Lecture Notes in Computer Science). Heidelberg: Springer. https://doi.org/10.1007/978-3-540-44616-3_12

A General Completeness Result in Refinement. / Kinoshita, Yoshiki; Power, John.

Recent Trends in Algebraic Development Techniques. Vol. 1827 Heidelberg : Springer, 2000. p. 201-218 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingChapter

Kinoshita, Y & Power, J 2000, A General Completeness Result in Refinement. in Recent Trends in Algebraic Development Techniques. vol. 1827, Lecture Notes in Computer Science, Springer, Heidelberg, pp. 201-218. https://doi.org/10.1007/978-3-540-44616-3_12
Kinoshita Y, Power J. A General Completeness Result in Refinement. In Recent Trends in Algebraic Development Techniques. Vol. 1827. Heidelberg: Springer. 2000. p. 201-218. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-44616-3_12
Kinoshita, Yoshiki ; Power, John. / A General Completeness Result in Refinement. Recent Trends in Algebraic Development Techniques. Vol. 1827 Heidelberg : Springer, 2000. pp. 201-218 (Lecture Notes in Computer Science).
@inbook{12a777435fd1460d9ffd0909873227b2,
title = "A General Completeness Result in Refinement",
abstract = "In a paper in 1986, Hoare, He and Sanders proposed a formulation of refinement for a system equivalent to the ν-calculus using a relation based semantics. To give a proof method to show that one program is a refinement of another, they introduced downward simulation and upward simulation, but the proof method based upon either of them is not complete with respect to their notion of refinement, so they claimed “joint” completeness based upon both notions of simulation with respect to their notion of refinement. We give a new definition of refinement in terms of structure respecting lax transformations, and show that the proof method based upon downward simulation is complete with respect to this notion of refinement. Although our theory works for the ν-calculus, we present the result for the μ-calculus to make the presentation simpler. We use results in enriched category theory to show this, and the central notion here is that of algebraic structure on locally ordered categories, not on sets. Our definition of refinement is neither a restriction nor a generalisation of Hoare, He and Sanders’ definition, but we include all their important examples.",
author = "Yoshiki Kinoshita and John Power",
year = "2000",
doi = "10.1007/978-3-540-44616-3_12",
language = "English",
volume = "1827",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "201--218",
booktitle = "Recent Trends in Algebraic Development Techniques",

}

TY - CHAP

T1 - A General Completeness Result in Refinement

AU - Kinoshita, Yoshiki

AU - Power, John

PY - 2000

Y1 - 2000

N2 - In a paper in 1986, Hoare, He and Sanders proposed a formulation of refinement for a system equivalent to the ν-calculus using a relation based semantics. To give a proof method to show that one program is a refinement of another, they introduced downward simulation and upward simulation, but the proof method based upon either of them is not complete with respect to their notion of refinement, so they claimed “joint” completeness based upon both notions of simulation with respect to their notion of refinement. We give a new definition of refinement in terms of structure respecting lax transformations, and show that the proof method based upon downward simulation is complete with respect to this notion of refinement. Although our theory works for the ν-calculus, we present the result for the μ-calculus to make the presentation simpler. We use results in enriched category theory to show this, and the central notion here is that of algebraic structure on locally ordered categories, not on sets. Our definition of refinement is neither a restriction nor a generalisation of Hoare, He and Sanders’ definition, but we include all their important examples.

AB - In a paper in 1986, Hoare, He and Sanders proposed a formulation of refinement for a system equivalent to the ν-calculus using a relation based semantics. To give a proof method to show that one program is a refinement of another, they introduced downward simulation and upward simulation, but the proof method based upon either of them is not complete with respect to their notion of refinement, so they claimed “joint” completeness based upon both notions of simulation with respect to their notion of refinement. We give a new definition of refinement in terms of structure respecting lax transformations, and show that the proof method based upon downward simulation is complete with respect to this notion of refinement. Although our theory works for the ν-calculus, we present the result for the μ-calculus to make the presentation simpler. We use results in enriched category theory to show this, and the central notion here is that of algebraic structure on locally ordered categories, not on sets. Our definition of refinement is neither a restriction nor a generalisation of Hoare, He and Sanders’ definition, but we include all their important examples.

UR - http://dx.doi.org/10.1007/978-3-540-44616-3_12

U2 - 10.1007/978-3-540-44616-3_12

DO - 10.1007/978-3-540-44616-3_12

M3 - Chapter

VL - 1827

T3 - Lecture Notes in Computer Science

SP - 201

EP - 218

BT - Recent Trends in Algebraic Development Techniques

PB - Springer

CY - Heidelberg

ER -