11Architecture and Design Intent© 2006, Dewayne E PerryLecture 4EE 382VPropagation Logic & Exception HandlingDewayne E PerryENS 623AOffice Hours: T/Th 11:00-12:00perry @ ece.utexas.eduwww.ece.utexas.edu/~perry/education/382v-s06/2Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VOne Direction of Inscape ResearchÎ Make practical use of specification and verification technologyªUse the module interface specifications in the construction of software systemsªImplement a semantic interconnection model that records unit, syntactic and semantic dependencies as the basis for evolutionªMake practical trade-offs between logic and analysis¾ how weak a logic?¾ how strong a form of consistency checking?Î Instress — the module interface specification languageªSpecification logic (SL), C syntax for declarationsªSL annotations for data object properties and operation interface behaviorÎ Inscape — using the specificationsªData object/operation specification instantiation¾ as the basis for the semantic interconnection and propagation¾ as a result of variable names and operation argumentsªPropagation logic (PL)¾ construct interfaces for sequence, selection, iteration¾ construct interfaces for implementations of operations3Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VGoals of AnalysisÎ Incremental AnalysisªUse specifications as a bootstrapping mechanism — ie, assume that they are correct and use themªAn operation is the gross grain of incremental analysis (the collection of operations individually analyzed forms the analysis of a module)ªA statement is the fine grain of incremental analysis (the goal is to be able to consider each statement independent of its surrounding context)Î Basic Rule:ªEvery precondition and obligation must either be satisfied within the implementation or propagated to its interface.4Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VSome Logical IntuitionÎ Separate consistencyfrom propagationªConsistency depends on trade-offs about how to manipulate the specification logicªPropagation depends on trade-offs bout how to statically represent a possible-execution tree as a single thread of knowledgeÎ Temptation to use orªIn reducing a possible-execution tree to a static (sequential) directed graph, how do you handle the results of joining two paths?ªSay Pis true in one path, Qin the other — one is tempted to describe the result as P or QªHowever, if not Plater becomes true, the inference of Qis not a valid one, because it might well have been the path that produced Pthat was actually executed.25Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VSome More IntuitionÎ Why we can treat each statement/operation as an indivisible unitªIntuitive picture of preconditions and postconditions¾ postconditions ‘‘sink down’’ through an implementation¾ preconditions ‘‘float up’’ through an implementation ‘‘looking’’ for satisfactionªAt the point where a precondition P occurs, either P is known to be true or false, or it is not known whether P is true or false¾ if P is true, then the precondition is satisfied (and it does not matter where in the preceding sequence it became true)¾ if P is false, P cannot be propagated to the interface and hence there is a problem with the implementation (it also does not matter where P became false, except to provide a range in which to fix the problem)¾ if P is unknown, then it is unknown ‘‘in’’ all of the preceding statements as wellªUnfortunately, obligations are not quite so tractable6Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VInscape’s Propagation Logic (PL)Î PL is a proposition calculus (SL is a predicate calculus with quantification) in whichªA proposition P is either true( P ) or false( ¬P )ªThe state of a proposition is either ¾unknown Pis not known to be either true or false in any execution path¾known Pis known to be true in all execution paths¾possible Pis known to be true in at least one execution pathªThere is one sentence connective, andªThere are the inference rules¾+seqa sequential addition or join based on the state of the propositions¾+para parallel addition or join based on the state of the propositions¾+cona sequential addition or join based on the consistency of the propositions7Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VInscape’s Propagation Logic (PL)Î Also used in the description of propagation areªSet theory operations: ∈, ∪, ∩, ⊂, ⊆, =, and −ªOperations from SL:¾consistentP is consistent with Q¾isknownP is known in Q8Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VThe Definition of +seqÎ P1 +seq P2 is defined as followsÎ Note: P +seq Q is not symmetricÎ The state of P2 supercedes the state of P1.ªwhatever is known in P2 supplants that of P1.ªwhatever in P1 is unknown in P2 retains its state from P1ªwhat is possible in P2 remains so in the result, but may also reduce what is know in P1 to a possible in the resultªexcept where it was known in P139Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VThe Definition of +parÎ P1 +par P2 is symmetric and defined as followsÎ Only what is known (unknown) to be true in both parts is known (unknown) to be true in a parallel join of the two parts. What is known in only one part becomes possible in the result.10Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VThe Definition of +con and -conÎ P1 +con P2 is defined as{p1...pk ∈ P1 | p1...pk are consistent P2} ∪ P2that is, the result of +con is P2 plus those propositions in P1 that are consistent with P2Î P1 -con P2 is defined asP1 - ( P1 +con P2 )that is, the result of -con are those propositions in P1 that are inconsistent with P211Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VThe Basis for Propagation12Architecture and Design IntentLecture 4© 2006, Dewayne E Perry EE 382VReasoning about SequencesÎ The following sets are used for reasoning about each Sequent Siin the Sequence S = S1.. SnPreithe set of preconditions for sequentiPostithe set of postconditions for sequentiOblithe set of obligations for sequentiPreCeilithe preconditions ceilinged by sequentiOblFloorithe obligations floored by sequentiStateithe current state after sequentiPromisedithe set of obligations outstanding after