Coverart for item
The Resource Verification of object-oriented software : the KeY approach, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (eds.) ; foreword by K. Rustan M. Leino

Verification of object-oriented software : the KeY approach, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (eds.) ; foreword by K. Rustan M. Leino

Label
Verification of object-oriented software : the KeY approach
Title
Verification of object-oriented software
Title remainder
the KeY approach
Statement of responsibility
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (eds.) ; foreword by K. Rustan M. Leino
Title variation
KeY approach
Contributor
Subject
Language
eng
Summary
Long gone are the days when program veri?cation was a task carried out merely by hand with paper and pen. For one, we are increasingly interested in proving actual program artifacts, not just abstractions thereof or core algorithms. The programs we want to verify today are thus longer, including whole classes and modules. As we consider larger programs, the number of cases to be considered in a proof increases. The creative and insightful parts of a proof can easily be lost in scores of mundane cases. Another problem with paper-and-pen proofs is that the features of the programming languages we employ in these programs are plentiful, including object-oriented organizations of data, facilities for specifying di?erent c- trol ?ow for rare situations, constructs for iterating over the elements of a collection, and the grouping together of operations into atomic transactions. These language features were designed to facilitate simpler and more natural encodings of programs, and ideally they are accompanied by simpler proof rules. But the variety and increased number of these features make it harder to remember all that needs to be proved about their uses. As a third problem, we have come to expect a higher degree of rigor from our proofs. A proof carried out or replayed by a machine somehow gets more credibility than one that requires human intellect to understand
Member of
Cataloging source
GW5XE
Dewey number
005.1/4
Illustrations
illustrations
Index
index present
LC call number
QA76.76.V47
LC item number
V474 2007eb
Literary form
non fiction
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorDate
1948-
http://library.link/vocab/relatedWorkOrContributorName
  • Beckert, Bernhard
  • Hähnle, Reiner
  • Schmitt, P. H.
Series statement
  • Lecture notes in computer science,
  • Lecture notes in artificial intelligence.
  • AI systems
Series volume
4334.
http://library.link/vocab/subjectName
  • Computer software
  • Object-oriented methods (Computer science)
  • Java (Computer program language)
  • Java (Computer program language)
  • Object-oriented methods (Computer science)
  • Computer software
  • Informatique
  • Computer software
  • Java (Computer program language)
  • Object-oriented methods (Computer science)
Label
Verification of object-oriented software : the KeY approach, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (eds.) ; foreword by K. Rustan M. Leino
Instantiates
Publication
Bibliography note
Includes bibliographical references (pages 627-643) and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
A New Look at Formal Methods for Software Construction -- A New Look at Formal Methods for Software Construction -- I: Foundations -- First-Order Logic -- Dynamic Logic -- Construction of Proofs -- II: Expressing and Formalising Requirements -- Formal Specification -- Pattern-Driven Formal Specification -- Natural Language Specifications -- Proof Obligations -- From Sequential Java to Java Card -- III: Using the KeY System -- Using KeY -- Proving by Induction -- Java Integers -- Proof Reuse -- IV: Case Studies -- The Demoney Case Study -- The Schorr-Waite-Algorithm -- Appendices -- Predefined Operators in Java Card DL -- The KeY Syntax
Control code
262693522
Dimensions
unknown
Extent
1 online resource (xxix, 658 pages)
Form of item
online
Isbn
9783540689775
Lccn
2006939067
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
9786611351519
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-540-68977-5
Specific material designation
remote
System control number
(OCoLC)262693522
Label
Verification of object-oriented software : the KeY approach, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (eds.) ; foreword by K. Rustan M. Leino
Publication
Bibliography note
Includes bibliographical references (pages 627-643) and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
A New Look at Formal Methods for Software Construction -- A New Look at Formal Methods for Software Construction -- I: Foundations -- First-Order Logic -- Dynamic Logic -- Construction of Proofs -- II: Expressing and Formalising Requirements -- Formal Specification -- Pattern-Driven Formal Specification -- Natural Language Specifications -- Proof Obligations -- From Sequential Java to Java Card -- III: Using the KeY System -- Using KeY -- Proving by Induction -- Java Integers -- Proof Reuse -- IV: Case Studies -- The Demoney Case Study -- The Schorr-Waite-Algorithm -- Appendices -- Predefined Operators in Java Card DL -- The KeY Syntax
Control code
262693522
Dimensions
unknown
Extent
1 online resource (xxix, 658 pages)
Form of item
online
Isbn
9783540689775
Lccn
2006939067
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
9786611351519
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-540-68977-5
Specific material designation
remote
System control number
(OCoLC)262693522

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
    • Engineering Library & Technology CommonsBorrow it
      W2001 Lafferre Hall, Columbia, MO, 65211, US
      38.946102 -92.330125
Processing Feedback ...