• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Refinement Algebra Extended with Operators for Enabledness and Termination

Kim Solin, Joakim von Wright, Refinement Algebra Extended with Operators for Enabledness and Termination. TUCS Technical Reports 658, Turku Centre for Computer Science, 2005.

Abstract:

Refinement algebras are axiomatisations intended for reasoning about programs in a total correctness framework. We reduce von Wright's demonic refinement algebra to only allow strong iteration and introduce two operators for modelling enabledness and termination of programs, respectively. We show how the operators can be used for expressing properties between programs and apply the algebra to reasoning about action systems.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tSovo05a,
  title = {Refinement Algebra Extended with Operators for Enabledness and Termination},
  author = {Solin, Kim and Wright, Joakim von},
  number = {658},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2005},
  keywords = {refinement algebra, total correctness, action systems, predicate transformers},
  ISBN = {952-12-1493-7},
}

Belongs to TUCS Research Unit(s): FUNDIM, Fundamentals of Computing and Discrete Mathematics, Learning and Reasoning Lab

Edit publication