| 000 -LEADER |
|---|
| fixed length control field |
04123nam a22005775i 4500 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| ISBN |
9783540690610 |
| -- |
978-3-540-69061-0 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
006.3 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Verification of Object-Oriented Software. The KeY Approach |
| Sub Title |
Foreword by K. Rustan M. Leino / |
| Statement of responsibility, etc |
edited by Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt. |
| 260 #1 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication |
Berlin, Heidelberg : |
| Name of publisher |
Springer Berlin Heidelberg, |
| Year of publication |
2007. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Number of Pages |
XXIX, 658 p. Also available online. |
| Other physical details |
online resource. |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Lecture Notes in Computer Science, |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
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. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc |
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. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Software engineering. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Logic design. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Artificial intelligence. |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Computer Science. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Artificial Intelligence (incl. Robotics). |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Logics and Meanings of Programs. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Mathematical Logic and Formal Languages. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Programming Languages, Compilers, Interpreters. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Software Engineering. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Beckert, Bernhard. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Hähnle, Reiner. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Schmitt, Peter H. |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Uniform Resource Identifier |
http://dx.doi.org/10.1007/978-3-540-69061-0 |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) |
|---|
| Koha item type |
E-BOOKS |
| 264 #1 - |
|---|
| -- |
Berlin, Heidelberg : |
| -- |
Springer Berlin Heidelberg, |
| -- |
2007. |
| 336 ## - |
|---|
| -- |
text |
| -- |
txt |
| -- |
rdacontent |
| 337 ## - |
|---|
| -- |
computer |
| -- |
c |
| -- |
rdamedia |
| 338 ## - |
|---|
| -- |
online resource |
| -- |
cr |
| -- |
rdacarrier |
| 347 ## - |
|---|
| -- |
text file |
| -- |
PDF |
| -- |
rda |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| -- |
0302-9743 ; |
