Back to Search
Start Over
Kleene under a modal demonic star
- Source :
- The Journal of Logic and Algebraic Programming. 66(2):127-160
- Publication Year :
- 2006
- Publisher :
- Elsevier BV, 2006.
-
Abstract
- In relational semantics, the input-output semantics of a program is a relation on its set of states. We generalise this in considering elements of Kleene algebras as semantical values. In a nondeterministic context, the demonic semantics is calculated by considering the worst behaviour of the program. In this paper, we concentrate on while loops. Calculating the semantics of a loop is difficult, but showing the correctness of any candidate abstraction is much easier. For deterministic programs, Mills has described a checking method known as the while statement verification rule. A corresponding programming theorem for nondeterministic iterative constructs is proposed, proved and applied to an example. This theorem can be considered as a generalisation of the while statement verification rule to nondeterministic loops. The paper generalises earlier relation-algebraic work to the setting of modal Kleene algebra, an extension of Kozen’s Kleene algebra with tests that allows the internalisation of weakest liberal precondition and strongest liberal postcondition operators.
- Subjects :
- Semantics (computer science)
Logic
Kleene's recursion theorem
0102 computer and information sciences
01 natural sciences
Theoretical Computer Science
Kleene algebra
While loop
Computer Science::Logic in Computer Science
Kleene star
0101 mathematics
Rule
Mathematics
Discrete mathematics
010102 general mathematics
Verification
Demonic semantics
Nondeterministic algorithm
Algebra
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Computational Theory and Mathematics
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Postcondition
Computer Science::Programming Languages
Kripke semantics
ddc:004
Relational abstraction
Generalisation
Computer Science::Formal Languages and Automata Theory
Software
Subjects
Details
- ISSN :
- 15678326
- Volume :
- 66
- Issue :
- 2
- Database :
- OpenAIRE
- Journal :
- The Journal of Logic and Algebraic Programming
- Accession number :
- edsair.doi.dedup.....36790673c2844536284ec48788139893
- Full Text :
- https://doi.org/10.1016/j.jlap.2005.04.006