View in EDS

Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language

Saved in:
Bibliographic Details
Title: Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language
Authors: Keimel, K., Rosenbusch, A. artus.ph.rosenbusch@gmail.com, Streicher, T.
Source: Theoretical Computer Science. Jun2011, Vol. 412 Issue 25, p2701-2713. 13p.
Subjects: Imperative programming, Denotational semantics, Predicate (Logic), Duality theory (Mathematics), Probability theory, Mathematical invariants, Isomorphism (Mathematics)
Abstract: Abstract: In Keimel et al. (2009)  we have systematically derived a predicate transformer semantics from a direct semantics in total correctness style for a nondeterministic/probabilistic basic imperative programming language . In the current paper we perform the analogous task starting from a direct semantics for in partial correctness style. As in  we establish a “Minkowski duality” providing an isomorphism between direct semantics and a continuation semantics from which a predicate transformer semantics can be read off immediately. But has only an auxiliary status and we use it to define a predicate transformer as capturing the idea of “weakest liberal preexpectation” (in analogy with weakest liberal precondition). We further explain why of while-loops is computed as a greatest fixpoint and argue why this allows one to reason about while-loops in terms of invariants as opposed to the of while-loops as considered in  for which this is impossible. [Copyright &y& Elsevier]
Copyright of Theoretical Computer Science is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 60161763
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Keimel%2C+K%2E%22">Keimel, K.</searchLink><br /><searchLink fieldCode="AR" term="%22Rosenbusch%2C+A%2E%22">Rosenbusch, A.</searchLink><i> artus.ph.rosenbusch@gmail.com</i><br /><searchLink fieldCode="AR" term="%22Streicher%2C+T%2E%22">Streicher, T.</searchLink>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Theoretical+Computer+Science%22">Theoretical Computer Science</searchLink>. Jun2011, Vol. 412 Issue 25, p2701-2713. 13p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Imperative+programming%22">Imperative programming</searchLink><br /><searchLink fieldCode="DE" term="%22Denotational+semantics%22">Denotational semantics</searchLink><br /><searchLink fieldCode="DE" term="%22Predicate+%28Logic%29%22">Predicate (Logic)</searchLink><br /><searchLink fieldCode="DE" term="%22Duality+theory+%28Mathematics%29%22">Duality theory (Mathematics)</searchLink><br /><searchLink fieldCode="DE" term="%22Probability+theory%22">Probability theory</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+invariants%22">Mathematical invariants</searchLink><br /><searchLink fieldCode="DE" term="%22Isomorphism+%28Mathematics%29%22">Isomorphism (Mathematics)</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Abstract: In Keimel et al. (2009)  we have systematically derived a predicate transformer semantics from a direct semantics in total correctness style for a nondeterministic/probabilistic basic imperative programming language . In the current paper we perform the analogous task starting from a direct semantics for in partial correctness style. As in  we establish a “Minkowski duality” providing an isomorphism between direct semantics and a continuation semantics from which a predicate transformer semantics can be read off immediately. But has only an auxiliary status and we use it to define a predicate transformer as capturing the idea of “weakest liberal preexpectation” (in analogy with weakest liberal precondition). We further explain why of while-loops is computed as a greatest fixpoint and argue why this allows one to reason about while-loops in terms of invariants as opposed to the of while-loops as considered in  for which this is impossible. [Copyright &y& Elsevier]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Theoretical Computer Science is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=60161763
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.tcs.2010.12.029
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 13
        StartPage: 2701
    Subjects:
      – SubjectFull: Imperative programming
        Type: general
      – SubjectFull: Denotational semantics
        Type: general
      – SubjectFull: Predicate (Logic)
        Type: general
      – SubjectFull: Duality theory (Mathematics)
        Type: general
      – SubjectFull: Probability theory
        Type: general
      – SubjectFull: Mathematical invariants
        Type: general
      – SubjectFull: Isomorphism (Mathematics)
        Type: general
    Titles:
      – TitleFull: Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Keimel, K.
      – PersonEntity:
          Name:
            NameFull: Rosenbusch, A.
      – PersonEntity:
          Name:
            NameFull: Streicher, T.
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 03
              M: 06
              Text: Jun2011
              Type: published
              Y: 2011
          Identifiers:
            – Type: issn-print
              Value: 03043975
          Numbering:
            – Type: volume
              Value: 412
            – Type: issue
              Value: 25
          Titles:
            – TitleFull: Theoretical Computer Science
              Type: main
ResultId 1