DISCRETE STRUCTURES II
DISCRETE STRUCTURES II CS 251
Popular in Course
Popular in ComputerScienence
This 1 page Class Notes was uploaded by Orrin Rutherford on Wednesday September 2, 2015. The Class Notes belongs to CS 251 at Portland State University taught by Staff in Fall. Since its upload, it has received 24 views. For similar materials see /class/168295/cs-251-portland-state-university in ComputerScienence at Portland State University.
Reviews for DISCRETE STRUCTURES II
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/02/15
Chapter 8 Axioms and Inference Rules Properties of Eguality for all terms t u and v any arbitrary function f and any arbitrary predicate p EA t t Symmetric t u 9 u t Transitive t u uv 9 tv EE functional form t u a f t f u EEpredicate form u p t 9p u EE for Wffs t u Wt9 Wu if t and u are free to replace x in Wx Assignment Axiom AA Pxt x t P The precondition is constructed from the post condition by replacing all free occurrences of x in P by t Array Assignment Axiom AAA P ai t Q where P is obtained from Q by 1 Replace all occurrences of ai in Q by t 2 Replace all occurrences of aj in Q by llifj i then t else ajquot Conseguence Rule P gtRandR SQ P ST andT gtQ P S Q P S Q Composition Rule P 51 Q and Q 52 R P Sl SZ R fThen and fThen Else Rules PACSQandP C gtQ PACS1QandPA CSZQ P if Cthen SQ P if Cthen S1 else S2 Q Whiledo Rule P is called the loop invariant P C SP P while C do S P C Termination Condition Find a wellfounded set W lt Find an expression f of the program variables Prove that if P and C are true for state s then fs ft E W and fs gt ft
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'