CSE3341

User Tools

Site Tools

You are here: W11-CSE3341M - Introduction to Program Verification » Course Outline
Trace:
course_outline

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
course_outline [2011/02/15 18:04] – jonathancourse_outline [2011/04/11 19:29] (current) – jonathan
Line 75: Line 75:
 ===== Week 7 - February 14 ===== ===== Week 7 - February 14 =====
  
-**Tuesday's Lecture**: Did a manual proof of the theorem needed for the theory of parity (in the ftp protocol). This theorem was hard to prove. The suggestion is to first do the proof manually, which then makes it easier to do in Rodin. Using this approach, we were able to derive a Lemma that was helpful in the Rodin proof. We also did the initial model of the celebrity example (from the Exercises). We showed how to formalize the problem in Event-B using a "knows" relation.  +**Tuesday's Lecture**: Did a manual proof of the theorem needed for the theory of parity (in the ftp protocol). This theorem was hard to prove. The suggestion is to first do the proof manually, which then makes it easier to do in Rodin. Using this approach, we were able to derive a Lemma that was helpful in the Rodin proof. We also did the initial model of the celebrity example (from the Exercises). We showed how to formalize the problem in Event-B using a "knows" relation. We dicussed the indentity and inverse relations and showed how the Celebrity axioms could be written in predicate logic or set theory. The celebrity example is one of the exercises that you must do in advance of Labtest1. [Challenge: In class we issued the following challenge: write a program given that takes as input a set of people and a knows relation, and outputs which person is the celebrity.   
  
-**Thursday's lecture**: Chapter 15: Development of sequential programs. Binary search. Merging Rules.+**Thursday's lecture**: First Refinement of Celebrity. Then we start Chapter 15: Development of sequential programs. Binary search. Merging Rules.
  
 Celebrity example ideas: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations. Celebrity example ideas: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations.
Line 120: Line 120:
 Tuesday: Data refinement and Procedural Refinement. Illustration of these concepts using the Birthday Book example in which we write an initial specification, do a data refinement, followed by a procedural refinement; finally a merge produces code. Tuesday: Data refinement and Procedural Refinement. Illustration of these concepts using the Birthday Book example in which we write an initial specification, do a data refinement, followed by a procedural refinement; finally a merge produces code.
  
-Thursday: Labtest2 +BAG abstract datatype.
  
 ===== Week 12===== ===== Week 12=====
course_outline.1297793064.txt.gz · Last modified: by jonathan