Verification of object-oriented software : (Record no. 637938)

MARC details
000 -LEADER
fixed length control field 07782cam a2201093 a 4500
001 - CONTROL NUMBER
control field ocn262693522
003 - CONTROL NUMBER IDENTIFIER
control field OCoLC
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20250703145449.0
006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS
fixed length control field m o d
007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION
fixed length control field cr cn|||||||||
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 081017s2007 gw a ob 001 0 eng d
010 ## - LIBRARY OF CONGRESS CONTROL NUMBER
Canceled/invalid LC control number 2006939067
040 ## - CATALOGING SOURCE
Original cataloging agency GW5XE
Language of cataloging eng
Description conventions pn
Transcribing agency GW5XE
Modifying agency HEBIS
-- OCLCQ
-- OCLCF
-- OCLCO
-- OCLCA
-- BEDGE
-- BUF
-- GZM
-- BAKER
-- COO
-- DAY
-- NUI
-- CNTRU
-- E7B
-- YDXCP
-- IDEBK
-- SLY
-- EBLCP
-- DEBSZ
-- OCLCQ
-- VT2
-- OCLCQ
-- ESU
-- U3W
-- STF
-- UAB
-- OCLCQ
-- CEF
-- MERER
-- OCLCQ
-- OCLCA
-- WYU
-- OCLCQ
-- YOU
-- OL$
-- OCLCQ
-- W2U
-- AUD
-- WURST
-- OCLCQ
-- EUX
-- OCLCQ
-- UKAHL
-- OCLCO
-- OCLCQ
-- OCL
-- OCLCQ
-- INARC
-- OCLCO
-- OCLCL
015 ## - NATIONAL BIBLIOGRAPHY NUMBER
National bibliography number 07,A17,0036
Source dnb
015 ## - NATIONAL BIBLIOGRAPHY NUMBER
National bibliography number 07,N07,0089
Source dnb
016 7# - NATIONAL BIBLIOGRAPHIC AGENCY CONTROL NUMBER
Record control number 982647239
Source DE-101
016 7# - NATIONAL BIBLIOGRAPHIC AGENCY CONTROL NUMBER
Record control number 985371226
Source DE-101
019 ## -
-- 123954273
-- 171130023
-- 272404612
-- 308298305
-- 320970268
-- 648193587
-- 696923568
-- 739147094
-- 880101573
-- 926292612
-- 964911693
-- 985043291
-- 1005772168
-- 1035662272
-- 1044334136
-- 1056374900
-- 1066435677
-- 1077995340
-- 1081180858
-- 1086845608
-- 1105589098
-- 1105599217
-- 1132302857
-- 1162795274
-- 1238604880
-- 1262676655
-- 1393050387
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783540690610
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 3540690611
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783540689775
Qualifying information (soft cover ;
-- alk. paper)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 354068977X
Qualifying information (soft cover ;
-- alk. paper)
024 8# - OTHER STANDARD IDENTIFIER
Standard number or code 9786611351519
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000042405727
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000048720480
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000051347389
029 1# - (OCLC)
OCLC library identifier DEBSZ
System control number 449581276
029 1# - (OCLC)
OCLC library identifier HEBIS
System control number 190419946
029 1# - (OCLC)
OCLC library identifier NLGGC
System control number 384199259
035 ## - SYSTEM CONTROL NUMBER
System control number (OCoLC)262693522
Canceled/invalid control number (OCoLC)123954273
-- (OCoLC)171130023
-- (OCoLC)272404612
-- (OCoLC)308298305
-- (OCoLC)320970268
-- (OCoLC)648193587
-- (OCoLC)696923568
-- (OCoLC)739147094
-- (OCoLC)880101573
-- (OCoLC)926292612
-- (OCoLC)964911693
-- (OCoLC)985043291
-- (OCoLC)1005772168
-- (OCoLC)1035662272
-- (OCoLC)1044334136
-- (OCoLC)1056374900
-- (OCoLC)1066435677
-- (OCoLC)1077995340
-- (OCoLC)1081180858
-- (OCoLC)1086845608
-- (OCoLC)1105589098
-- (OCoLC)1105599217
-- (OCoLC)1132302857
-- (OCoLC)1162795274
-- (OCoLC)1238604880
-- (OCoLC)1262676655
-- (OCoLC)1393050387
037 ## - SOURCE OF ACQUISITION
Stock number 978-3-540-68977-5
Source of stock number/acquisition Springer
Note http://www.springerlink.com
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA76.76.V47
Item number V474 2007eb
072 #7 - SUBJECT CATEGORY CODE
Subject category code QA
Source lcco
082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number 005.1/4
Edition number 22
084 ## - OTHER CLASSIFICATION NUMBER
Classification number TP311. 5
Number source clc
049 ## - LOCAL HOLDINGS (OCLC)
Holding library MAIN
245 00 - TITLE STATEMENT
Title Verification of object-oriented software :
Remainder of title the KeY approach /
Statement of responsibility, etc. Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (eds.) ; foreword by K. Rustan M. Leino.
246 30 - VARYING FORM OF TITLE
Title proper/short title KeY approach
260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Place of publication, distribution, etc. Berlin ;
-- New York :
Name of publisher, distributor, etc. Springer,
Date of publication, distribution, etc. ©2007.
300 ## - PHYSICAL DESCRIPTION
Extent 1 online resource (xxix, 658 pages) :
Other physical details illustrations
336 ## - CONTENT TYPE
Content type term text
Content type code txt
Source rdacontent
337 ## - MEDIA TYPE
Media type term computer
Media type code c
Source rdamedia
338 ## - CARRIER TYPE
Carrier type term online resource
Carrier type code cr
Source rdacarrier
490 1# - SERIES STATEMENT
Series statement Lecture notes in computer science,
International Standard Serial Number 0302-9743 ;
Volume/sequential designation 4334.
Series statement Lecture notes in artificial intelligence.
-- AI systems
504 ## - BIBLIOGRAPHY, ETC. NOTE
Bibliography, etc Includes bibliographical references (pages 627-643) and index.
588 0# - SOURCE OF DESCRIPTION NOTE
Source of description note Print version record.
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 or geographic name as entry element Computer software
General subdivision Verification.
9 (RLIN) 1930
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Object-oriented methods (Computer science)
9 (RLIN) 15626
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Java (Computer program language)
9 (RLIN) 15662
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer programs
General subdivision Verification.
9 (RLIN) 17233
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Logiciels
General subdivision Vérification.
9 (RLIN) 20690
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Conception orientée objet (Informatique)
9 (RLIN) 966777
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Java (Langage de programmation)
9 (RLIN) 19336
650 07 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Java (Computer program language)
Source of heading or term cct
9 (RLIN) 15662
650 07 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Object-oriented methods (Computer science)
Source of heading or term cct
9 (RLIN) 15626
650 07 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Verification.
Source of heading or term cct
9 (RLIN) 1930
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Informatique.
Source of heading or term eclas
9 (RLIN) 14930
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer programs
General subdivision Verification
Source of heading or term fast
9 (RLIN) 17233
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Verification
Source of heading or term fast
9 (RLIN) 1930
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Java (Computer program language)
Source of heading or term fast
9 (RLIN) 15662
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Object-oriented methods (Computer science)
Source of heading or term fast
9 (RLIN) 15626
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term wiskunde
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term mathematics
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term computerwetenschappen
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term computer sciences
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term kunstmatige intelligentie
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term artificial intelligence
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term logica
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term logic
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term programmeertalen
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term programming languages
653 00 - INDEX TERM--UNCONTROLLED
Uncontrolled term software engineering
653 10 - INDEX TERM--UNCONTROLLED
Uncontrolled term Information and Communication Technology (General)
653 10 - INDEX TERM--UNCONTROLLED
Uncontrolled term Informatie- en communicatietechnologie (algemeen)
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Beckert, Bernhard.
9 (RLIN) 25348
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Hähnle, Reiner.
9 (RLIN) 25349
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Schmitt, P. H.
Fuller form of name (Peter H.),
Dates associated with a name 1948-
-- https://id.oclc.org/worldcat/entity/E39PBJjhD3c44V39xckh6W8wG3
9 (RLIN) 30124
758 ## -
-- has work:
-- Verification of object-oriented software (Text)
-- https://id.oclc.org/worldcat/entity/E39PCGr9DcPbFdyyBXJftJghBK
-- https://id.oclc.org/worldcat/ontology/hasWork
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Print version:
Title Verification of object-oriented software.
Place, publisher, and date of publication Berlin ; New York : Springer, ©2007
International Standard Book Number 9783540689775
-- 354068977X
Record control number (DLC) 2006939067
-- (OCoLC)78203745
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture notes in computer science ;
Volume number/sequential designation 4334.
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture notes in computer science.
Name of part/section of a work Lecture notes in artificial intelligence.
9 (RLIN) 14916
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture notes in computer science.
Name of part/section of a work Lecture notes in artificial intelligence.
-- AI systems.
9 (RLIN) 29029
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier <a href="https://link.springer.com/10.1007/978-3-540-69061-0">https://link.springer.com/10.1007/978-3-540-69061-0</a>
938 ## -
-- Askews and Holts Library Services
-- ASKH
-- AH26903051
938 ## -
-- Baker & Taylor
-- BKTY
-- 89.95
-- 89.95
-- 354068977X
-- 0007169589
-- active
938 ## -
-- ProQuest Ebook Central
-- EBLB
-- EBL3036596
938 ## -
-- ebrary
-- EBRY
-- ebr10171190
938 ## -
-- ProQuest MyiLibrary Digital eBook Collection
-- IDEB
-- cis23786937
938 ## -
-- YBP Library Services
-- YANK
-- 2595082
938 ## -
-- Internet Archive
-- INAR
-- isbn_9783540689775
994 ## -
-- 92
-- ATIST
Holdings
Withdrawn status Lost status Damaged status Not for loan Collection code Home library Current library Date acquired Total Checkouts Date last seen Price effective from Koha item type
  Not Lost     eBook LNCS e-Library e-Library 28/07/2022   28/07/2022 28/07/2022 eBook

Powered by Koha