LEADER 03760nam  22006855  450 
001 996465760403316
005 20200706022039.0
010   $a3-540-69539-7
024 7 $a10.1007/BFb0027453
035   $a(CKB)1000000000234702
035   $a(SSID)ssj0000324932
035   $a(PQKBManifestationID)11268448
035   $a(PQKBTitleCode)TC0000324932
035   $a(PQKBWorkID)10320520
035   $a(PQKB)11488332
035   $a(DE-He213)978-3-540-69539-4
035   $a(PPN)155196626
035   $a(EXLCZ)991000000000234702
100   $a20121227d1997      u|             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aModular Compiler Verification$b[electronic resource] $eA Refinement-Algebraic Approach Advocating Stepwise Abstraction /$fby Markus Müller-Olm
205   $a1st ed. 1997.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1997.
215   $a1 online resource (XVI, 260 p.) 
225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1283
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-63406-1 
327   $aComplete Boolean lattices -- Galois connections -- States, valuation functions and predicates -- The algebra of commands -- Communication and time -- Data refinement -- Transputer base model -- A small hard real-time programming language -- A hierarchy of views -- Compiling-correctness relations -- Translation theorems -- A functional implementation -- Conclusion.
330   $aThis book presents the verified design of a code generator translating a prototypic real-time programming language to an actual microprocessor, the Inmos Transputer. Unlike most other work on compiler verification, and with particular emphasis on modularity, it systematically covers correctness of translation down to actual machine code, a necessity in the area of safety-critical systems. The formal framework provided as well as the novel proof-engineering ideas incorporated in the verified code generator are also of relevance for software design in general.
410  0$aLecture Notes in Computer Science,$x0302-9743 ;$v1283
606   $aProgramming languages (Electronic computers)
606   $aArchitecture, Computer
606   $aSoftware engineering
606   $aComputer logic
606   $aSpecial purpose computers
606   $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037
606   $aComputer System Implementation$3https://scigraph.springernature.com/ontologies/product-market-codes/I13057
606   $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029
606   $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X
606   $aSpecial Purpose and Application-Based Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I13030
615  0$aProgramming languages (Electronic computers).
615  0$aArchitecture, Computer.
615  0$aSoftware engineering.
615  0$aComputer logic.
615  0$aSpecial purpose computers.
615 14$aProgramming Languages, Compilers, Interpreters.
615 24$aComputer System Implementation.
615 24$aSoftware Engineering.
615 24$aLogics and Meanings of Programs.
615 24$aSpecial Purpose and Application-Based Systems.
676   $a005.4/53
700   $aMüller-Olm$b Markus$4aut$4http://id.loc.gov/vocabulary/relators/aut$0508822
906   $aBOOK
912   $a996465760403316
996   $aModular compiler verification$91489174
997   $aUNISA