Library

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Book
    Book
    Patterns for parallel programming / (2005)
    Boston [u.a.] :Addison-Wesley,
    Details
    Title: Patterns for parallel programming /
    Author: Mattson, Timothy G.
    Contributer: Sanders, Beverly A. , Massingill, Berna L.
    Publisher: Boston [u.a.] :Addison-Wesley,
    Year of publication: 2005
    Pages: XIII, 355 S. : , graph. Darst.
    Series Statement: ¬The¬ software patterns series
    ISBN: 0-321-22811-1
    Type of Medium: Book
    Language: English
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    ZIB Catalog
    Zuse Institute Berlin get availability status
  • 2
    Electronic Resource
    Electronic Resource
    Eliminating the substitution axiom from UNITY logic (1991)
    Springer
    Formal aspects of computing 3 (1991), S. 189-205 
    Details
    ISSN: 1433-299X
    Keywords: UNITY ; Substitution axiom ; Program composition ; Completeness
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The UNITY substitution axiom, “if (x=y) is an invariant of a program, then x can be replaced by y in any property of the program”, is problematic for several reasons. In this paper, dual predicate transformerssst andwst are introduced that allow the strongest invariant of a program to be expressed, and these are used to give new definitions for the temporal operatorsunless andensures. With the new definitions, the substitutionaxiom is no longer needed, and can be replaced by a derived rule of inference which is formally justified in the logic. One important advantage is that the effects of the initial conditions on the properties of a program are formally captured in a convenient way, and one can forget about substitution in formal treatments of the UNITY proof system while still having it available when desirable to use during the derivation of programs. Composibility and completeness of the modified logic are also discussed.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01898402
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    A predicate transformer for the progress property ‘to-always’ (1997)
    Springer
    Formal aspects of computing 9 (1997), S. 270-282 
    Details
    ISSN: 1433-299X
    Keywords: Progress ; Predicate transformer ; ‘to-always’ ; ‘leads-to’ ; Nondeterministic dataflow ; Fault-tolerance
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The temporal property ‘to-always’ has been proposed for specifying progress properties of concurrent programs. Although the ‘to-always’ properties are a subset of the ‘leads-to’ properties for a given program, ‘to-always’ has more convenient proof rules and in some cases more accurately describes the desired system behavior. In this paper, we give a predicate transformerwta, derive some of its properties, and use it to define ‘to-always’. Proof rules for ‘to-always’ are derived from the properties ofwta. We conclude by briefly describing two application areas, nondeterministic data flow networks and self-stabilizing systems where ‘to-always’ properties are useful.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01211085
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Electronic Resource
    Electronic Resource
    Data refinement of mixed specifications (1998)
    Springer
    Acta informatica 35 (1998), S. 91-129 
    Details
    ISSN: 1432-0525
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract. Using predicate transformers as a basis, we give semantics and refinement rules for mixed specifications that allow UNITY style specifications to be written as a combination of abstract program and temporal properties. From the point of view of the programmer, mixed specifications may be considered a generalization of the UNITY specification notation to allow safety properties to be specified by abstract programs in addition to temporal properties. Alternatively, mixed specifications may be viewed as a generalization of the UNITY programming notation to allow arbitrary safety and progress properties in a generalized ‘always section’. The UNITY substitution axiom is handled in a novel way by replacing it with a refinement rule. The predicate transformers foundation allows known techniques for algorithmic and data-refinement for weakest precondition based programming to be applied to both safety and progress properties. In this paper, we define the predicate transformer based specifications, specialize the refinement techniques to them, demonstrate soundness, and illustrate the approach with a substantial example.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/s002360050115
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...