{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:07:35Z","timestamp":1725566855824},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540236115"},{"type":"electronic","value":"9783540304722"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30472-2_1","type":"book-chapter","created":{"date-parts":[[2010,9,23]],"date-time":"2010-09-23T16:07:39Z","timestamp":1285258059000},"page":"1-16","source":"Crossref","is-referenced-by-count":1,"title":["A Beginner\u2019s Course on Reasoning About Imperative Programs"],"prefix":"10.1007","author":[{"given":"Kung-Kiu","family":"Lau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"1_CR2","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J. Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)"},{"key":"1_CR3","unstructured":"Barwise, J., Etchemendy, J.: The Language of First Order Logic, 3rd edn. CSLI (1993)"},{"key":"1_CR4","unstructured":"Extended Static Checking for Java Home Page, \n                  \n                    http:\/\/research.compaq.com\/SRC\/esc\/"},{"key":"1_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"Gries, D.: The Science of Programming. Springer, Heidelberg (1981)"},{"key":"1_CR6","volume-title":"The Unified Software Development Process","author":"I. Jacobson","year":"1999","unstructured":"Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison-Wesley, Reading (1999)"},{"key":"1_CR7","unstructured":"The Java Modeling Language (JML) Home Page, \n                  \n                    http:\/\/www.cs.iastate.edu\/~leavens\/JML.html"},{"key":"1_CR8","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice Hall, Englewood Cliffs (1990)","edition":"2"},{"key":"1_CR9","volume-title":"The Programming Process: An Introduction using VDM and Pascal","author":"J.T. Latham","year":"1990","unstructured":"Latham, J.T., Bush, V.J., Cottam, I.D.: The Programming Process: An Introduction using VDM and Pascal. Addison-Wesley, Reading (1990)"},{"key":"1_CR10","unstructured":"Lau, K.-K.: CS1112: Reasoning about Programs, \n                  \n                    http:\/\/www.cs.man.ac.uk\/~kung-kiu\/cs1112\/"},{"key":"1_CR11","volume-title":"The Unified Modeling Language Reference Manual","author":"J. Rumbaugh","year":"1999","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading (1999)"},{"key":"1_CR12","unstructured":"SPARKAda, Praxis Critical Systems Limited, \n                  \n                    http:\/\/www.praxis-cs.co.uk\/sparkada\/"},{"key":"1_CR13","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)","edition":"2"},{"key":"1_CR14","unstructured":"Tarski\u2019s World, \n                  \n                    http:\/\/wwwcsli.stanford.edu\/hp\/Tarski1.html"}],"container-title":["Lecture Notes in Computer Science","Teaching Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30472-2_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:02:27Z","timestamp":1620000147000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30472-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540236115","9783540304722"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30472-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}