Library

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
    London u.a. :Academic Press,
    Title: GPS: a case study in generality and problem solving
    Author: Ernst, George W.
    Contributer: Newell, Allen
    Publisher: London u.a. :Academic Press,
    Year of publication: 1969
    Pages: 297 S.
    Series Statement: ACM monograph series
    Type of Medium: Book
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 2
    Electronic Resource
    Electronic Resource
    Springer
    Acta informatica 18 (1982), S. 149-169 
    ISSN: 1432-0525
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Summary A verification system is developed for proving the correctness of programs containing procedures with procedure-type parameters. The system, which reduces programs and their specifications to assertions to be proved in ordinary logic, is shown to be logically sound. The reduction process is controlled by the syntax of the program and is completely mechanical, requiring no human intervention. The resulting assertions involve higher-order predicates, but they engender no significant difficulties which are not already present in ordinary first-order theories. Our system views the intermediate objects in the reduction process as extended programs, thereby making verification a much less abstruse process. Treating logical assertions as commands appeals strongly to a programmer's intuition.
    Type of Medium: Electronic Resource
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 3
    Electronic Resource
    Electronic Resource
    Springer
    Acta informatica 8 (1977), S. 145-152 
    ISSN: 1432-0525
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Summary The semantics of procedures and parameters were formalized by Hoare [2] in terms of axioms and rules of inference. Igarashi et al. [4] reformulated Hoare's system. This paper extends their rule of inference for procedure calls to allow i) actual variable parameters to occur in actual value parameters; ii) the body of a procedure to contain global variables that do not occur in assignment positions; iii) post-conditions and “internal” assertions of a procedure to refer to the initial values of variable parameters. None of these are allowed in Hoare's system or the system of Igarashi, London and Luckham. An attractive feature of these extensions is that they do not increase the complexity of the rules of inference.
    Type of Medium: Electronic Resource
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...