# Axiomatising the Logic of Computer Programming by R. Goldblatt By R. Goldblatt

Read or Download Axiomatising the Logic of Computer Programming PDF

Best programming languages books

Programming Language Pragmatics (3rd Edition)

Programming Language Pragmatics is the main accomplished programming language textbook to be had at the present time. Taking the viewpoint that language layout and language implementation are tightly interconnected, and that neither might be absolutely understood in isolation, this seriously acclaimed and bestselling booklet has been completely up-to-date to hide the newest advancements in programming language layout.

The Foundations of Program Verification

The rules of application Verification moment version Jacques Loeckx and Kurt Sieber Fachbereich informatik Universitat des Saariandes, Saarbrucken, Germany In collaboration with Ryan D. Stansifer division of desktop technological know-how Cornell college, united states This revised version offers an exact mathematical history to numerous software verification thoughts.

Graph-Based Proof Procedures for Horn Clauses

Preliminaries. - A Semantics for the Hornlog method. - The Hornlog facts method. - Soundness and Completeness effects I. - An Equational Extension. - The He � Refutation procedure. - Soundness and Completeness effects II. - Appendix: Implementation concerns.

VHDL Design Representation and Synthesis

-- comprises a very transparent creation to based layout recommendations and layout instruments. -- grasp the ASlC layout procedure and key implementation applied sciences: PLDs, FPGAs, gate arrays, and conventional cells. -- New! CD-ROM includes the book's VHDL versions, version try out benches, and homework suggestions.

Additional info for Axiomatising the Logic of Computer Programming

Example text

R := g]~ will be explicitly Thus our system constitutes something of a departure even in its treatment of the standard quantifiers. EQUIVALENCE OF PROGRAMS. As an instance of r C a ++ [r := a]~ we have reflecting the fact that the command (r := r) changes nothing, and so is "equivalent" to S ~ p . But the latter satisfies ~-~ [ s k i p ] ~ and so [r is valid. e. that they halt for the same inputs and bring about the same output situations. g. that a w ~ e - c o m m a n d 29 is equivalent to the dummy command ~hen its test expression is false.

L ~ -~ ( [ w h / / e is valid. Hence ~ do a ]~ ++ q~) We shall modify this slightly below, after m a k i n g a d i s t i n c t i o n between i n t e r n a l and e x t e r n a l v e r s i o n s of negation. ASSIGNMENTS. In the new notion the Rule of A s s i g n m e n t becomes r ~ ~ [ r := ~]~, b u t the intuition that suggests that this is v a l i d does the same to [r := ~]~ ~ r , and h e n c e to ~r +~ [ r := ~]~ (this w i l l be m o d i f i e d b e l o w to allow for the p o s s i b i l i t y that ~ has no value).

V s(f0/~e) = 0 2. if Vs(a) = CO vs(e ~ 8,~) = vs(6) if VS(a) = I vs (~) if VS (~) = 0 to the 40 3. If either v~e 6) Vs{e) or L Us(h) is ~), then I if V8(£) = V8(6) 0 if VS(e) ~ Vs(£ = otherwise 6) is 09; U8(6). Writing DE as an abbreviation for (e = e), from clause 3 we have 7 ~0 if VS(e) = 03 Vs and hence v s(true) = v s(Df~g~e) = I. The interpretation of the connective m is the (see McCarthy (1963), Manna and McCarthy of McCarthy (1970)), in which we imagine the computer first evaluating e and then proceeding to 6 or 2.