ࡱ> AM<=>?@( / 00DArialngsITC0XX 0DComic Sans MS0XX 0B DEras Demi ITC0XX 0"0DWingdingsITC0XX 0 A .  @n?" dd@  @@``   8 &pi 5  21  21..HH,, 21  g5hjmox{}*65   9!               ! 0AA0 f%%@TJK+L- ʚ;0ʚ;g4pdpdK 0ppp@  <4dddd$l 0X<4!d!d$l 0X<42d2d$l 0X<___PPT10 66___PPT9{?8$ $Tutorial at FM2005O  =)The Spec# Programming System: An OverviewGTutor: Bart Jacobs PhD student at K.U.Leuven, Belgium Spec# contributorHZH" What is Spec#?('A programming language that extends C# with specification constructs A compiler that emits run-time checks for the specification constructs A static verifier that modularly proves that the run-time checks never fail An environment with base class library contracts and a Visual Studio extension |'ZZ1?> BB7 Spec# GoalsMake it easier to record detailed design decisions Provide tools to enforce these decisions Help prevent and detect bugs Reduce cost of software lifecycle @\$ Demo: The Bag ClassDemonstrates Non-null types Method contracts (including out-of-band contracts for system libraries) Loop invariants The object invariant methodology The static verifier" ZZTutorialWhat is Spec#? Non-null types Method contracts Object invariants Ownership  Break Inheritance State Abstraction MultithreadingHKZZ-ZK-G;TutorialWhat is Spec#? Non-null types Method contracts Object invariants Ownership  Break Inheritance State Abstraction MultithreadinglKZZ-Z--.$Non-null typesEach reference type T includes the value null Spec# s type T! contains only references to objects of type T (not null).z -.E/%Types versus AssertionsWithout non-null types: Person(string name) requires name != null; With non-null types: Person(string/*^!^*/ name) [Q] What is the difference?P/PP8P    , 7 +0&!Non-null types are flow-sensitive""(The non-null type of an expression is flow-sensitive. void Foo(T o) { if (o != null) T! p = o; // OK! } That is, it does not follow uniquely from the declared types of the variables and members mentioned in the expression.7PP8w=4*#Non-null Fields and Object Creation3class C { public C() { ((D) this).f.Foo(); } } X40Z  `class D : C { T! f; D(T! x) : base() { f = x; } } [Q] Can this be unsound? [A] Yes! >a ;I<Non-nullness of Fields QCommon coding pattern: if (o.f != null) o.f.Foo(); [Q] How can this go wrong?LR ,  y]Non-nullness of Properties(QCommon coding pattern: if (o.P != null) o.P.Foo(); [Q] How can this go wrong?LR ,  z^Fields and Properties8For the non-null dataflow analysis, we assume that non-nullness of fields and properties is preserved in the absence of intervening heap-modifying operations Property reads are not considered heap-modifying operations But we check this at run time because of the possibility of Data races Impure property getters.Z#Z#7J=TutorialWhat is Spec#? Non-null types Method contracts Object invariants Ownership  Break Inheritance State abstraction MultithreadinglKZZ-Z- Preconditionsstatic int Divide(int a, int b) { if (b==0) throw new ArgumentException(); return a / b; } [Q] What s wrong with this? static int Divide(int a, int b) /*^requires b != 0;^*/ { return a / b; } Throws a RequiresException if false. But how can we get full backwards compatibility? static int Divide(int a, int b) requires b != 0 otherwise ArgumentException; { return a / b; }pPWPcP    =  % 9 7D "N@Checked Exceptionsint Eval(Expr e) throws EvalErrorException; Alternative: bool TryEval(Expr e, out int value, out string errorMessage) + explicit propagation through recursive calls0ZZsZ  1~    3 Definedness of contracts  public static int BinarySearch (int[] a, int value) ensures result < a.Length; ensures a[result] == value; [Q] What if result < 0 ? This contract is ill-defined. In Spec#, an ill-defined contract is considered an error. If at run time, evaluation of a contract clause throws an exception, the exception is wrapped in an InvalidContractException and propagated. For static checking, the program verifier generates an error if it cannot prove that a contract is well-defined.Z  ]%PBTutorialZWhat is Spec#? Non-null types Method contracts Intermezzo: Inside the Spec# Program Verifier Object invariants Ownership  Break Inheritance State abstraction MultithreadinglyPP-P/.-  From Spec#...(static int Abs(int x) ensures 0 <= x ==> result == x; ensures x < 0 ==> result == -x; { if (x < 0) x = -x; return x; }      ,n& via BoogiePL & aprocedure Abs(x$in: int) returns ($result: int); ensures 0 <= x$in ==> $result == x$in; ensures x$in < 0 ==> $result == -x$in; { var x1, x2: int, b: bool; entry: x1 := x$in; b := x < 0; goto t, f; t: assume b; x := -x; goto end; f: assume !b; goto end; end: $result := x; return; }bZ   $"/  ),9&& via BoogiePL-DSA & nprocedure Abs(x$in: int) returns ($result: int); ensures 0 <= x$in ==> $result == x$in; ensures x$in < 0 ==> $result == -x$in; { var x1, x2: int, b: bool; entry: x1 := x$in; b := x1 < 0; goto t, f; t: assume b; x2 := -x1; goto end; f: assume !b; x2 := x1; goto end; end: $result := x2; return; }oZ   $" '2  0/<{_.& via Passive BoogiePL &  procedure Abs(x$in: int) returns ($result: int); ensures 0 <= x$in ==> $result == x$in; ensures x$in < 0 ==> $result == -x$in; { var x1, x2: int, b: bool; entry: assume x1 == x$in; assume b == x1 < 0; goto t, f; t: assume b; assume x2 == -x1; goto end; f: assume !b; assume x2 == x1; goto end; end: assume $result == x2; return; }>P   $"  $"  ;76Cc*& without contracts & procedure Abs(x$in: int) returns ($result: int); ensures 0 <= x$in ==> $result == x$in; ensures x$in < 0 ==> $result == -x$in; { var x1, x2: int, b: bool; entry: assume x1 == x$in; assume b == x1 < 0; goto t, f; t: assume b; assume x2 == -x1; goto end; f: assume !b; assume x2 == x1; goto end; end: assume $result == x2; return; }>P   $"  $"  ;76C}`*& without contracts & procedure Abs(x$in: int) returns ($result: int); { var x1, x2: int, b: bool; entry: assume x1 == x$in; assume b == x1 < 0; goto t, f; t: assume b; assume x2 == -x1; goto end; f: assume !b; assume x2 == x1; goto end; end: assume $result == x2; assert 0 <= x$in ==> $result == x$in; assert x$in < 0 ==> $result == -x$in; return; }>P     $/k  ;76BW~b& to Logic[M. Barnett, K. R. M. Leino, in preparation] entry && (entry <== (x1 == x$in ==> b == x1 < 0 ==> t && f)) && (t <== (b ==> x2 == -x1 ==> end)) && (f <== (!b ==> x2 == x1 ==> end)) && (end <== ($result == x2 ==> (0 <= x$in ==> $result == x$in) && (x$in < 0 ==> $result == -x$in) && true))PPBbMWRCTutorialWhat is Spec#? Non-null types Method contracts Object invariants Ownership  Break Inheritance State abstraction MultithreadinglKZZ-Z/ -UFObject Invariantsclass Word { private string! line; int start, length; public string ToString() { return line.Substring(start, length); } } [Q] How can we prove ToString?P ' P%"(uObject Invariantsclass Word { private string! line; int start, length; invariant 0 <= start && 0 <= length; invariant start + length <= line.length; public string ToString() { return line.Substring(start, length); } } [Q] How can we prove ToString?P8   Lb%U (& Re-entrancyclass Subject { & invariant & ; Observer d; void Foo(& ) { // invariant assumed & if (& ) d.Notify(& ); & // invariant reestablished } }P  ',@G5 class Observer { & Subject c; void Notify(& ) { & if (& ) c.Foo(& ); & } }|P%$`f Re-entrancyclass Subject { & invariant I; Observer d; void Foo(& ) requires I; { // invariant assumed & if (& ) d.Notify(& ); & // invariant reestablished } }P  ,@S5 class Observer { & Subject c; void Notify(& ) { & if (& ) c.Foo(& ); & } }|P|`d"Spec# Object Invariant Methodology##(bEach object gets a boolean field inv Regular fields may be modified only when inv is false inv field may be modified only using special BeginExpose() and EndExpose() calls BeginExpose() sets inv to false EndExpose() checks invariant; if it holds, sets inv to true; otherwise, throws ObjectInvariantException Therefore, if inv is true, the invariant holds\cP!)*    %tn    F0eExposing objectsJclass Subject { & invariant & ; Observer d; void Foo(& ) requires inv; { & // uses invariant (sound!) BeginExpose(); & // field updates if (& ) d.Notify(& ); & // restores invariant EndExpose(); } }&P & 1P@B G2  'Exposing objects6class Subject { & invariant & ; Observer d; void Foo(& ) requires inv; { & // uses invariant (sound!) expose (this) { & // field updates if (& ) d.Notify(& ); & // restores invariant } } } P  1,@< class Observer { & Subject c; void Notify(& ) { & if (& ) c.Foo(& ); & } } b}P%.`iObject Invariants: Example(class Word { private string! line; private int start; public int length; invariant 0 <= start && 0 <= length; invariant start + length <= line.length; public void SelectPart(int start, int length) requires inv; requires 0 <= start && 0 <= length; requires length <= this.length; ensures inv; { expose (this) { this.start += start; this.length = length; } } }dP     "       -N V -  t%Object Invariants and Object Creation&&(class Word { private string! line; private int start; public int length; invariant 0 <= start && 0 <= length; invariant start + length <= line.Length; public Word(string! line, int start, int length) requires 0 <= start && 0 <= length; requires start + length <= line.Length; ensures inv; { this.line = line; this.start = start; this.length = length; base(); EndExpose(); } }P       %$ !/R  X    #  jObject Invariants: Recap<Spec# supports object invariants To avoid reentrancy problems, we introduce an inv field; it abstracts the invariant and may be used in contracts BeginExpose() and EndExpose() calls (or expose blocks) toggle inv; they delimit the regions where the invariant does not need to hold and where the object may be modified=ZO@   j,  hInvariants and Exceptions(pclass EOFException : CheckedException {} byte ReadByte() throws EOFException { expose (this) { & if (& ) throw EOFException(); & } }P)#b   B gInvariants and Exceptions(void Foo(int a, int b) { expose (this) { & & a / b & & } }[ 2,HsXTutorialWhat is Spec#? Non-null types Method contracts Object invariants Ownership  Break Inheritance State abstraction Multithreading^KZZ-ZA -[HInter-object Invariants<class Account { List deposits; int balance; invariant balance == Math.Sum(deposits); public List GetDeposits() { return deposits; } public static List GetAllDeposits(Account a1, Account a2) { List ds = a1.GetDeposits(); ds.AddRange(a2.GetDeposits()); return ds; } }L=P  # 4@ ! 3CmInter-object InvariantsDclass Account { [Owned] List deposits; int balance; invariant balance == Math.Sum(deposits); public List GetDeposits() { return deposits; } public static List GetAllDeposits(Account a1, Account a2) { List ds = a1.GetDeposits(); ds.AddRange(a2.GetDeposits()); return ds; } }EP ! 3CoInter-object InvariantsDclass Account { [Owned] List deposits; int balance; invariant balance == Math.Sum(deposits); public List GetDeposits() { return deposits; } public static List GetAllDeposits(Account a1, Account a2) { List ds = a1.GetDeposits(); ds.AddRange(a2.GetDeposits()); return ds; } }EP ! 3CqUpdating Owned Objectsclass Account { [Owned] List deposits; int balance; invariant balance == Math.Sum(deposits); void Deposit(int amount) { expose (this) { deposits.Add(amount); balance += amount; } } }P % Wb!# /4wObject Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();vP  L@<        xObject Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();P/@<        yObject Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();jP6 @<        zObject Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();jPE@<        {Object Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();ZPU@<        |Object Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();ZPe/<        }Object Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();jPe<        ~Object Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();jPe"<        Object Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();ZPe1<        Object Lifecycle// Account a = new Account(); Account a = new Account; List<int> d = new List<int>; d.EndExpose(); a.deposits = d; a.EndExpose(); // a.Deposit(& ); a.BeginExpose(); d.BeginExpose(); d.EndExpose(); a.EndExpose();NPe@<        r IsExposable ho.IsExposable means o.inv == true && o.owner == null class List<T> { void Add(T value) requires IsExposable; ensures IsExposable; { expose (this) { & } } },5PP  l  #   pOwnership SystemFEach object has an inv field and an owner field o.owner == null means that o is currently not owned o.owner == p means that p owns o o.IsExposable means o.inv == true && o.owner == null o.BeginExpose() requires o.IsExposable An object points to its component objects using [Owned] fields o.EndExpose() assigns o as the owner of o s component objects o.BeginExpose() sets the owner field of o s component objects to nulljP '    0 120-    @  tYTutorialWhat is Spec#? Non-null types Method contracts Object invariants Ownership  Break Inheritance State abstraction Multithreading^KZZ-ZK !( Subclassing class Account { invariant true; public int balance; public void Add(int n) requires IsExposable; { expose (this) { balance += n; } } }P    '>/ 5 =class StudentAccount : Account{ invariant 0 <= balance; }F>P *Subclassing as Containment(  Subclassing as Containment( class Account { invariant true; public int balance; public void Add(int n) requires IsExposable; { expose (this) { balance += n; } } }P    '>/ 5 Uclass StudentAccount { invariant 0 <= base.balance; [Owned] Account! base; }FVP 2,  Learning from Containment(  Subclassing class Account { invariant true; public int balance; public void Add(int n) requires IsExposable; { expose (this) { balance += n; } } }P    '>/ 5 =class StudentAccount : Account{ invariant 0 <= balance; }F>P *hOVirtual methodsclass Account { public int balance; public void Add(int n) { expose (this) balance += n; } public virtual bool TryAdd(int n) { Add(n); return true; } }~Pg b;   class StudentAccount { invariant 0 <= balance; public override bool TryAdd(int n) { if (balance + n < 0) return false; expose (this) return base.TryAdd(n); } } P3  P3 R -##Modular verification of inheritance$$$class Account { public int balance; public void Add(int n) requires IsExposable; { expose (this) { balance += n; } } public virtual bool TryAdd(int n) requires IsVirtualExposable; { Add(n); return true; } }PD%" >  class StudentAccount { invariant 0 <= balance; public override bool TryAdd(int n) { if (balance + n < 0) return false; expose (this) { return base.TryAdd(n); } } }JP  P4 _  )  Inheritance uZTutorialWhat is Spec#? Non-null types Method contracts Object invariants Ownership  Break Inheritance State abstraction MultithreadinglKZZ-ZK  Pure Methods [Pure] static int Double(int x) ensures result == x + x; static int Quadruple(int x) ensures result == Double(Double(x)); { return 4 * x; } [Q] How does one verify this statically? For each pure method, a function symbol is defined. For each ensures clause of a pure method, an axiom is added. function Double(int) returns (int); axiom (forall x:int, heap: & :: Double(heap, x) == x + x);P       )     State Abstractionclass StudentAccount { private int balance; invariant 0 <= balance; public int Balance { get { return balance; } } public void Deposit(int amount) requires 0 <= Balance + amount; { expose (this) { balance += amount; } } }BP      P26 `State Abstractionclass StudentAccount { private int balance; invariant 0 <= balance; public int Balance { get ensures result == balance; { return balance; } } public void Deposit(int amount) requires 0 <= Balance + amount; { expose (this) { balance += amount; } } }BP     P2U `State AbstractionTclass StudentAccount { private int balance; invariant 0 <= balance; public int Balance { get private ensures result == balance; { return balance; } } public void Deposit(int amount) requires 0 <= Balance + amount; ensures Balance == old(Balance) + amount; { expose (this) { balance += amount; } } }BUP     Pb2] L ;8. State Abstraction and Interfacesinterface IList { int Count { get; } T this[int i] { get; } public void Add(T x) ensures Count == old(Count) + 1; ensures forall{int i in (0:old(Count)); this[i] == old(this[i])}; ensures this[old(Count)] == x; }, P            #   v[TutorialWhat is Spec#? Non-null types Method contracts Object invariants Ownership  Break Inheritance State abstraction Multithreading^KZZ-ZKpUMultithreadingAccount a = new Account(); new Thread(delegate { a.Deposit(1000); }).Start(); new Thread(delegate { a.Deposit(1000); }).Start(); [Q] What s wrong with this? Solution: we need to ensure that a thread has exclusive access to an object when it accesses the object.     !, $MultithreadingWhat if we redefine expose (o) so that it additionally locks o? Account a = new Account(); Account b = new Account(); new Thread(delegate { a.Deposit(-1000); b.Deposit(1000); }).Start(); new Thread(delegate { a.Deposit(-1000); b.Deposit(1000); }).Start(); [Q] What s wrong with this? Conclusion: We need a separate construct for locking an object. aA  23^,|6rWMultithreadingAccount a = new Account(); a.EndAcquire(); new Thread(delegate { acquire (a) a.Deposit(1000); }).Start(); new Thread(delegate { acquire (a) a.Deposit(1000); }).Start(); We achieve mutual exclusion by extending the notion of ownership: an object may now be owned by another object or by a thread. It may also be free (i.e. not owned by any thread or object). Formally, the owner field may be either null (which means that the object is free), an object, or a thread. A o.BeginAcquire(); call performed by a thread t waits until o is free and then assigns ownership of o to t. An o.EndAcquire(); call releases ownership of o; o becomes free. An o.IsExposable call performed by a thread t means: o.owner == t && o.inv == true. "#k  0X` 5 %  MultithreadingAccount a = new Account(); Account b = new Account(); new Thread(delegate { acquire (a) { acquire (b) { a.Deposit(-1000); b.Deposit(1000); }}}).Start(); new Thread(delegate { acquire (a) { acquire (b) { a.Deposit(-1000); b.Deposit(1000); }}}).Start();0  @@,;^ZMultithreadingclass BankServer { Account! account; public void Run() { while (true) { int amount = AcceptDepositRequest(); acquire (account) { account.Deposit(amount); } } } & }P( .[P T 4(@5Readers-Writersclass StatementPrinter { Account! account; public void Run() { while (true) { Thread.Sleep(30*24*3600*1000); acquire readonly (account) { PrintStatement(account.Balance); } } } & }  P. ;e>*A6Wait Conditionsclass BankServer { StudentAccount! account; public void Run() { int amount = AcceptDepositRequest(); acquire (account; 0 <= account.Balance + amount) { account.Deposit(amount); } } & }Pt + #w\ Thank You!JDownload papers and alpha bits at http://research.microsoft.com/specsharp/KK) /hFKQSXZ_ ijkm| J1  0` fp=` f3` 33f` 3f33` 3f3f` fff3` f3` 3|f>?" dd@,|?" dd@   " @ ` n?" dd@   @@``PV    @ ` `p>>  --p44,(    BW CfDE,F6 W  Pn n /Hf  W W @`""  S y " 0  NClick toMaster title style    C { "   RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  C Ȃ "``  F*0  C  "`   H*0  C ̌ "`8  H*0  B_ CwDE,F6  12w  _  `@`"55^   B C DE F*    FRj @`"%wT  i   " iV   BCDE`Fj3R3[J3d =xjXy.|7 sb"3324@`" Y:   BCDEF"x@`" E   B2C5DE0F: 3~25Fy+**. @`",X  BCDE F*ENEE@`"V  BCDE F*$ @`" lE  BCDEF"H@`"C  BCDE F*PWPP@`"  BC\DEF&j\+@`"  B8CDEFN8 @`"[mb  i # " ib   # "   B9CDE(F2 kr $9[CJe kk@`"Z  BC DE$F. ( G((@`"|)  BWCDE$F. $],PWt.@`" _  BCDEF"d4dd@`"L  BC(DE@FJ"BDF2Pk(x"""$@`".  BCDE(F2 [PjGaX9@`"5`Nb  iH # " iH  BCDE F*n(BPgTnn@`"'`  "BCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`"OH  BCODE$F. tj!:^OLtt@`"ja   BCDE8FB|Q&9+Cca=wJL2 @`"  ! BCDE,F6 Lq>thc;?@`"BB> " BC DE4F> )B@  tMY)) @`"H.  # BCDE4F> _N95_}H9 @`" i $ BCDE@FJ~Bt*n Lp_55 n~~~"$@`"lT \5O % "5\O &B ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"\< ) 'B ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"5O x T 9B ( "9B b 9B )# "9B * BC&DE F*{ V&Ox{ { @`"T\ 9B + "9B , B\C]DE$F. *]\g @`"t9F - B(CDEXFb`M;Bl (TDAkl`^tZ?v.0@`"d . BC DEF" =@`"6zsn / 0B CDElFv_  5  o } 6 +   N ? T iS/x9 h  r [  u _ _ 8<@`"B 0 BCVDE F*PjV!rPP@`"iC 1 BCDE F*NT~(rFNN@`"( 2 BCDE F*N<:W6NN@`"v 3 BCDE F*X425+XX@`"iy,hB 4 s *DԔ"T0B  s *޽h ? fp=80___PPT10.; Crayons J 0 YQ(    BC#DEF" y#e  @`"   <_)3 Ԕ8c?"` P   T Click to edit Master title style! !  C a) " p  ) W#Click to edit Master subtitle style$ $  C f) "`` ) F*0  C (k) "`  ) H*0  C tp) "`  ) H*0T z N[   " zN[   zBCDE0F: >,GS:@`" E   zB2C5DE0F: 3~25Fy+**. @`" 5   zBCDE F*ENEE@`"  \ z N[   "z N[   zBCDE F*n(BPgTnn@`"zw  f  (zBCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`" [   zBCDEF"d4dd@`"Z!    zBCODE$F. tj!:^OLtt@`"U N   zBC(DE@FJ"BDF2Pk(x"""$@`"= L $  C BCDELF$)+,04k|w@xy( @  E@      "p 8; F {8  "{@\ {   "{    BCDE0F: >,GS:@`"{    B2C5DE0F: 3~25Fy+**. @`"j    BCDE F*ENEE@`"X\ {    "{    BCDE F*n(BPgTnn@`"|f  (BCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`"{   BCDEF"d4dd@`"D  BCODE$F. tj!:^OLtt@`"|  BC(DE@FJ"BDF2Pk(x"""$@`"N   B0CDE(F| fYc 0 @   " 8 B  s *޽h ? fp=80___PPT10.;V1  0` fp=` f3` 33f` 3f33` 3f3f` fff3` f3` 3|f>?" dd@,|?" dd@   " @ ` n?" dd@   @@``PR    @ ` ` p>> &-- 44,(    BW CfDE,F6 W  Pn n /Hf  W W @`""  S ) "`P ) T Click to edit Master title style! !   C ) "  ) RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  C X) "`` ) F*0  C ) "`  ) H*0  C ? "`8 ? H*0  B_ CwDE,F6  12w  _  `@`"55^   B C DE F*    FRj @`"%wT  i   "$@V   BCDE`Fj3R3[J3d =xjXy.|7 sb"3324@`" Y:   BCDEF"x@`" E   B2C5DE0F: 3~25Fy+**. @`",X  BCDE F*ENEE@`"V  BCDE F*$ @`" lE  BCDEF"H@`"C  BCDE F*PWPP@`"  BC\DEF&j\+@`"  B8CDEFN8 @`"[mb  i # " ib   # "   B9CDE(F2 kr $9[CJe kk@`"Z  BC DE$F. ( G((@`"|)  BWCDE$F. $],PWt.@`" _  BCDEF"d4dd@`"L  BC(DE@FJ"BDF2Pk(x"""$@`".  BCDE(F2 [PjGaX9@`"5`Nb  iH # " iH  BCDE F*n(BPgTnn@`"'`  "BCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`"OH  BCODE$F. tj!:^OLtt@`"ja   BCDE8FB|Q&9+Cca=wJL2 @`"  ! BCDE,F6 Lq>thc;?@`"BB> " BC DE4F> )B@  tMY)) @`"H.  # BCDE4F> _N95_}H9 @`" i $ BCDE@FJ~Bt*n Lp_55 n~~~"$@`"lT \5O % "5\O &B ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"\< ) 'B ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"5O x T 9B ( "9B b 9B )# "9B * BC&DE F*{ V&Ox{ { @`"T\ 9B + "9B , B\C]DE$F. *]\g @`"t9F - B(CDEXFb`M;Bl (TDAkl`^tZ?v.0@`"d . BC DEF" =@`"6zsn / 0B CDElFv_  5  o } 6 +   N ? T iS/x9 h  r [  u _ _ 8<@`"B 0 BCVDE F*PjV!rPP@`"iC 1 BCDE F*NT~(rFNN@`"( 2 BCDE F*N<:W6NN@`"v 3 BCDE F*X425+XX@`"iy,hB 4 s *DԔ"T0B  s *޽h ? fp=D<___PPT10..; 1_CrayonsJ 0 zr0 (    0? P   ? P*    0$?    ? R*  d  c $ ?  ?  0'?  0 ? RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  6x-? _P  ? P*    61? _  ? R*  H  0޽h ? 3380___PPT10./B6K 0  0(  x  c $ )` P  ) x  c $h) p  ) H  0޽h ? 33___PPT10i..M+D='  = @B + J 0 P0(  x  c $B? 0  ? x  c $B?  ? H  0޽h ? 33___PPT10i.2g+D='  = @B +U J 0 ld (  ~  s *T? 0  ? ~  s *T?  ? X2  0 0 X2  0  H  0޽h ? 33___PPT10i.8 |+D='  = @B + J 0 (0(  (x ( c $\c? 0  ? x ( c $ d?  ? H ( 0޽h ? 33___PPT10i.5@f+D='  = @B + J 0 @0(  x  c $q? 0  ? x  c $q?  ? H  0޽h ? 33___PPT10i./p+D='  = @B + J 0 p <(  ~  s *? 0  ? ~  s *>?  ? H  0޽h ? 33___PPT10i./p+D='  = @B + J 0 (*(  (x ( c $? 0  ? r ( S t?  ? H ( 0޽h ? fp=___PPT10i."F+D='  = @B + J 0 ,*(  ,x , c $ ? 0  ? r , S ?  ? H , 0޽h ? fp=___PPT10i.1S-+D='  = @B + J 0 0*(  0x 0 c $? 0  ? r 0 S p?  ? H 0 0޽h ? fp=___PPT10i.F+D='  = @B +-% J 0  HT(  Hx H c $$? 0  ?  H S $?@ ` <$  0 ?  H S $? <$D 0 ?  H C ? ` ` ,$  0 >class D : C { T! f; D(T! x) { f = x; base(); } }>? ,  H 6"`P ,$D   0 H 0@ p,$@  0H H 0޽h ? fp=  ___PPT10. GMY+/LDM' ?= @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*HV`%(D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*H %(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*H D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*H D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*H %(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*H D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*H D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*H1%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*H1D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*H1D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*H13%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*H13D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*H13D ' =%(D ' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*H%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*HD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*HD' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*HD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*HD' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*H%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*HD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*H+p+0+H0 ++0+H0 +} J 0  $(  r  S  ? 0  ? r  S ?  ? H  0޽h ? fp=___PPT10i.+D='  = @B + J 0  0(  x  c $? 0  ? x  c $?  ? H  0޽h ? fp=___PPT10i.+D='  = @B + J 0L0  6(  ~  s *? 0  ? x  c $?  ? H  0޽h ? fp=___PPT10i.`OL+D='  = @B + J 0  <(  ~  s *4 B 0  B ~  s * B  B H  0޽h ? 33___PPT10i./p+D='  = @B +D  J 0 V(  x  c $2) 0  )   S 3) <$@ 0 ) H  0޽h ? fp=&  ___PPT10 .=% 6+ED '  = @B D ' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*y%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*:%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*:}%(+ J 0  6(  ~  s *B 0  B x  c $B  B H  0޽h ? fp=___PPT10i.ePa+D='  = @B + J 0 <\(  <x < c $ 'B 0  B  < c $ (B <$@ 0 B H < 0޽h ? 33___PPT10.DT+EDZ'  = @B D' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*<%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*<%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*<%(+ J 0  <(  ~  s * :B 0  B ~  s *:B  B H  0޽h ? 33___PPT10i./p+D='  = @B + J 0 D0(  Dx D c $HB 0  B x D c $`IB  B H D 0޽h ? 33___PPT10i.D`{+D='  = @B + J 0 *(  x  c $QB 0  B r  S RB  B H  0޽h ? fp=___PPT10i._@+D='  = @B + J 0 6(  ~  s *eB 0  B x  c $fB  B H  0޽h ? fp=___PPT10i._@+D='  = @B + J 0 6(  ~  s *l{B 0  B x  c $0|B@ B H  0޽h ? fp=___PPT10i._@+D='  = @B + J 0 p6(  ~  s *@B 0  B x  c $B@ B H  0޽h ? fp=___PPT10._@+D' = @B D[' = @BA?%,( < +O%,( < +D' =%(D:' =%(D5' =4@BB@BB%()?)?D' =.Q7 BBBBBcM -3.33333E-6 4.44444E-6 L -3.33333E-6 -0.11112 *3>*B ppt_xB ppt_y=@0BBAApBBB9c<*D+' =4@BB@BB%()?)?D' =.G7 BBBBBYM 3.33333E-6 4.44444E-6 L 0.00295 -0.10116 *3>*B ppt_xB ppt_y=@0BBAApBBa :BO<*D-' =4@BB@BB%()?)?D' =.I7 BBBBB[M -2.77778E-6 -3.7037E-7 L -0.00382 -0.0919 *3>*B ppt_xB ppt_y=@0BBAApBBOBv<<*D#' =4@BB@BB%()?)?Dw' =.?7 BBBBBQM -0.01198 0.00718 L -0.01198 -0.10393 *3>*B ppt_xB ppt_y=@0BBAApBBB9c<*?D#' =4@BB@BB%()?)?Dw' =.?7 BBBBBQM -0.01146 0.00324 L -0.01024 -0.10648 *3>*B ppt_xB ppt_y=@0BBAApBB:B `<*?yD' =4@BB@BB%()?)?Do' =.77 BBBBBIM 0 3.33333E-6 L -0.00295 -0.09931 *3>*B ppt_xB ppt_y=@0BBAApBB̺BK<*yD' =4@BBBB%()?)?D2' =.7 BBBBB3M 0 0 L 0.09288 0.37384 *3>*B ppt_xB ppt_y=0BBAA<*1\D' =4@BBBB%()?)?D2' =.7 BBBBB3M 0 0 L 0.09288 0.37384 *3>*B ppt_xB ppt_y=0BBAA<*\+ J 0  6(  ~  s *dB 0  B x  c $+B#style.visibility<*8_%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*8_D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*8_D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*_%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*_D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*_+1 J 0 2*(  x  c $C 0  C x  c $XC  C   S XCX  <$  0 C   0C 6,$D  0 P[Q] What could go wrong here? ==> Let s drop the assumption that invariants hold on method entry. [Q] But then, when can we assume they hold? 2H  0޽h ? fp=,,___PPT10,.Јp~+(LDl,' C= @B D',' = @BA?%,( < +O%,( < +D&' =%(D&' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*&%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*&D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*&D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*&;%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*&;D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*&;D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*;E%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*;ED' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*;ED' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*ET%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*ETD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*ETD' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*Tj%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*TjD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*TjD' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*jt%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*jtD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*jtD' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*tz%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*tzD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*tzD' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*z|%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*z|D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*z|D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*b%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*b%(+8+0+0 +V J 0 h`(  ~  s *=C 0  C ~  s *=C  C x  c $>CX   C 4  04@C 6,$D 0 P[Q] Can we simply require that the invariant holds? No! This breaks abstraction!4Q 28H  0޽h ? fp=___PPT10n.Јp~+ DB'  = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4Q%(+} J 0 $(  r  S ]C 0  C r  S x^C  C H  0޽h ? fp=___PPT10i.fZ:+D='  = @B + J 0 .&(  ~  s *nC 0  C ~  s *hC w C r  S i%X   C H  0޽h ? fp=___PPT10i.Јp~+D='  = @B +g8 J 0L0 (  ~  s *C 0  C ~  s *`C w C   c $`CX  <$  0 C :   fԉCGxfHwIbJ~ KVL~ M7cN   =,$D   0 p:Yes! This call is not allowed; precondition does not hold!; ;  0+B#style.visibility<*%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*&%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*&D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*&D' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*&;%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*&;D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*&;D' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*;E%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*;ED' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*;ED' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*ET%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*ETD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*ETD' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*Tj%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*TjD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*TjD' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*jt%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*jtD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*jtD' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*tz%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*tzD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*tzD' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*z|%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*z|D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*z|D' =A@BBBB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?dCB1+#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*++0+0 ++0+0 ++0+0 + J 0 (  ~  s *4C 0  C x  c $ Cm C 3   fCGHIiJ KLMN   ,$D  0 i+A method typically requires and ensures inv", (   fCG HI!gJ@K!gLL MVNL  ` 2 ,$D  0 =Also, the body is typically wrapped in an expose (this) blockb> )H  0޽h ?/  fp=  ___PPT10 .c + D ' C= @B D ' = @BA?%,( < +O%,( < +D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*+p+0+0 ++0+0 + J 0 /(  r  S C 0  C r  S C@ C   6|C"` 0,$D 0 [When an object is created, its inv field is false. The constructor typically initializes the fields, establishing the invariant, and then calls EndExpose() to set the inv field.l  _   H  0޽h ? fp=___PPT10.)+ksDO'  = @B D ' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(+8+0+0 +} J 0 $(  r  S  G 0  G r  S tG  G H  0޽h ? fp=___PPT10i.O+D='  = @B +b  J 0 x(  x  c $G 0  G x  c $G  G @  0hG w,$@ 0 [Q] Should the expose block perform an EndExpose() if the body terminates with a checked exception? Yes  throwing a checked exception does not mean the object is broken. Future calls on the object need to be able to rely on the invariant. Note that if the invariant does not hold, the EndExpose() call replaces the checked exception with an ObjectInvariantException.lp 2  ->'  /H  0޽h ? fp="___PPT10.0x+AGD'  = @B D' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(+  J 0 C;(  r  S P>G 0  G r  S (?G  G   0t@G  ,$@ 0 E[Q] Should the expose block perform an EndExpose() if the body terminates with an unchecked exception? No --- the object is broken. Leaving it exposed will prevent future method calls on the object. Also, performing an EndExpose() might replace the original exception with an ObjectInvariantException, masking the real error.lF 2  .>'  0H  0޽h ? fp="___PPT10.0x+AGD'  = @B D' = @BA?%,( < +O%,( < +D' =%(Dh' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*g%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*F%(+ J 0  l(  l~ l s *L^G 0  G  l  6_G "6 ?  G H l 0޽h ? 33___PPT10i./p+D='  = @B +/ J  0  !(  ~  s *TlG 0  G   c $TmG <$@ 0 G   0nG0  E[Q] Is this okay? 2   frGGHIJKLMIN ~ ? ,$D   0 Oops! This modifies a1 s list of deposits. Also, a1 s invariant is now broken.@P >  64zG"`  x,$D   0 bSpec# solution: Allow the list of deposits to be modified only when the account object is exposed.c cH  0޽h ? fp=))___PPT10).cL^+@D(' G= @B D(' = @BA?%,( < +O%,( < +D' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*a%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*aD' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*aD' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*(D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(7%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*(7D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*(7D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*7;%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*7;D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*7;D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?dCB1+#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*+p+0+0 ++0+0 +  J 0 yqP(  ~  s *G 0  G x  c $G  &   0HG0  E[Q] Is this okay? 2   f(GGHIJKLMIN ~ ?  Oops! This modifies a1 s list of deposits. Also, a1 s invariant is now broken.@P    6G"`  x bSpec# solution: Allow the list of deposits to be modified only when the account object is exposed.c c\  6XG"` ,$D  0 jThis is achieved by having the account object own the list of deposits whenever the former is not exposed..k .:H  0޽h ? fp=5-___PPT10 .cL^+?˜D' G= @B Dd' = @BA?%,( < +O%,( < +D' =%(%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?dCB0-#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*+8+0+0 +c  J 0 aY(  ~  s * G 0  G x  c $G  G   00G0  E[Q] Is this okay? 2   fGGHIJKLMIN ~ ?  Oops! This modifies a1 s list of deposits. Also, a1 s invariant is now broken.@P    6G"`  x bSpec# solution: Allow the list of deposits to be modified only when the account object is exposed.c c(  6@G"`  jThis is achieved by having the account object own the list of deposits whenever the former is not exposed..k .:  6G"`E2r ,$D 0 lds.BeginExpose() fails if ds is owned, so AddRange won t succeed in modifying ds.^R  H H  0޽h ? fp=___PPT10.cL^+{ 9D'  = @B D' = @BA?%,( < +O%,( < +D' =%(%(D' =%(D@' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-o6Bdissolve*<3<*+8+0+0 +z J 0 '(  r  S \I 0  I r  S IN I :  6I"``@ #,$D  0 ^Objects cannot be modified while they re owned.0 0M  6<I"` @ - ,$D  0 OBut calling BeginExpose() on the owner releases ownership of the owned objects.P P 9d  6I"`0 @ 70,$D  0 fCalling O.EndExpose() causes O to (re-)gain ownership of the objects pointed to by its [Owned] fields.g g TH  0޽h ? fp=___PPT10c.`>+nD' %I= @B DJ' = @BA?%,( < +O%,( < +D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?dCB1+#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?dCB1+#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?dCB1+#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*++0+0 ++0+0 ++0+0 + J 0 -%@ (   x   c $8I 0  I ~   s *t9I  I    0I  A exposed exposable ownedX( 2 %%H   0޽h ? fp=___PPT10i.04+D='  = @B + J 0  @(  @x @ c $RI 0  I ~ @ s *SI  I 2 @ <TI@ p0 Za inv == false owner == null"  @ 0VIpW , 2 @ 0^I  A exposed exposable ownedX( 2 %%H @ 0޽h ? fp=___PPT10i.04+D='  = @B + J 0  DY(  Dx D c $lqI 0  I ~ D s *DrI  I 2 D <sI@p  Zd inv == false owner == null" 2 D <uI@ p0 Za inv == false owner == null"  D 0LIpW , 2 D 0xI  A exposed exposable ownedX( 2 %%H D 0޽h ? fp=___PPT10i.04+D='  = @B +) J 0 @8 H(  Hx H c $ȔI 0  I ~ H s *I  I 2 H <I%%@p  qd inv == true owner == null: 2 H <I@ p0 Za inv == false owner == null"  H 0ܘIpW , 2 H 0 I  A exposed exposable ownedX( 2 %%X"  H 0@@H H 0޽h ? fp=___PPT10i.04+D='  = @B + J 0 & L(  Lx L c $@I 0  I ~ L s *I  I 2 L <PI%%@p  Yd inv == true owner == null" 2 L <@I@ p0 Za inv == false owner == null"  L 0IpW , 2 L 0I  A exposed exposable ownedX( 2 %%RB  L s *D @   L 0I   <deposits 2 X"  L 0@@H L 0޽h ? fp=___PPT10i.04+D='  = @B + J 0  P8(  PX" P 0 @ x P c $I 0  I ~ P s *I  I 2 P <I@p  dd inv == true owner == a0 2 P <@I%%@ p0 qa inv == true owner == null:  P 0IpW , 2 P 0I  A exposed exposable ownedX( 2 %%RB  P s *D @   P 0I   <deposits 2 X"  P 0@@H P 0޽h ? fp=___PPT10i.04+D='  = @B + J 0 4, T(  Tx T c $  0   ~ T s *h   2 T <%%@p  gd inv == true owner == null0 2 T <@ p0 Za inv == false owner == null"  T 0pW , 2 T 0  A exposed exposable ownedX( 2 %%RB  T s *D @   T 0<%   <deposits 2 X"  T 0@@H T 0޽h ? fp=___PPT10i.04+D='  = @B + J 0   Xo(  Xx X c $(6 0   ~ X s *6   2 X <88@p  rd inv == false owner == null: 2 X <H?@ p0 Za inv == false owner == null"  X 0(:pW , 2 X 0\G  A exposed exposable ownedX( 2 %%RB  X s *D @   X 0N   <deposits 2 H X 0޽h ? fp=___PPT10i.04+D='  = @B +' J 0 >60 \(  \x \ c $_ 0   ~ \ s *_   2 \ <$a%%@p  qd inv == true owner == null: 2 \ <0h@ p0 Za inv == false owner == null"  \ 0cpW , 2 \ 0Dp  A exposed exposable ownedX( 2 %%RB  \ s *D @   \ 0hw   <deposits 2 X"  \ 0@@H \ 0޽h ? fp=___PPT10i.04+D='  = @B + J 0 @ `8(  `X" ` 0  @ x ` c $ 0   ~ ` s *x   2 ` <Ċ@p  dd inv == true owner == a0 2 ` <%%@ p0 qa inv == true owner == null:  ` 0pW , 2 ` 0  A exposed exposable ownedX( 2 %%RB  ` s *D @   ` 0   <deposits 2 X"  ` 0@@H ` 0޽h ? fp=___PPT10i.04+D='  = @B + J 0 F(  r  S  0   r  S l     6"`P @ 8A method typically requires and ensures this.IsExposable09 ( (H  0޽h ? fp=___PPT10i.C+D='  = @B +} J 0 $(  r  S ș 0   r  S ș   H  0޽h ? fp=___PPT10i.p+D='  = @B + L 0  p(  p~ p s *8֙`P    p  6`ҙ "6 ?   H p 0޽h ? 33___PPT10i./p+D='  = @B + J 0 Q(  x  c $8 0   x  c $   r  S ۙX 0     S    Qstatic void MyAdd(Account a, int n) requires a.IsExposable; { a.Add(n); // breaks StudentAccount invariant! } StudentAccount s = new StudentAccount(); MyAdd(s, -1000); [Q] How can we fix this? How can we translate this into something that we already know? P  %    dH  0޽h ? fp=___PPT10i.׈`+D='  = @B +u  J 0   Pd (  dr d S  0   2 d <ppp0  0 f d 0"`ppX2 d 0 ppf d 0"`0ppX2 d 0ppLB  d c $D0ppLB  d c $D0pp  d 0t `w A Account frame 2  d 0\%`pt  bStudentAccount frame 2F d 0d) P X  jclass Account { & } class StudentAccount : Account {}>6 2X d 00 p ^" d 6 :2 d Bt2  0 2 d B6:   , XB d 0D:^" d 69M5 d 0$9P BAccount object 2 d 0$=P`t  cStudentAccount object 2d d 0,A 0   class Account { & } class StudentAccount { [Owned] Account base; }>E 2,H d 0޽h ? fp=___PPT10i.3P-{+D='  = @B +z J 0 `h!(  h~ h s *L 0   ~ h s *M   x h c $NX 0   ] h C Q  ` static void MyAdd(StudentAccount s, int n) requires s.IsExposable; { s.base.Add(n); // requires fails: Account object is not exposable } StudentAccount s = new StudentAccount(); MyAdd(s, -1000); P %2=   :  H h 0޽h ? fp=___PPT10i.׈`+D='  = @B +h  J 0  w p (  pX" p 00 x p c $} 0   2 p <0%%ppp0  0 f p 0%%"`ppX2 p 0 ppf p 0"`0ppX2 p 0ppLB p c $D0ppLB  p c $D0pp  p 0`w A Account frame 2  p 0艚`pt  bStudentAccount frame 2X  p@ 00 p X" p 0 :2 p <䏚  0 2 p <ȓ%%:   , RB p s *D:X" p 09M5 p 0 P BAccount object 2 p 0䚚P`t  cStudentAccount object 2X" p 0px  p 08 `  Each frame has its own inv field and owner field Therefore, each frame has its own non-virtual IsExposable property Each frame owns its base class frame Therefore, the ownership system enables a subclass to safely mention the state of its base classn 2  Q}a H p 0޽h ? fp=___PPT10i.3P-{+D='  = @B +V J  0 met(  t~ t s *' 0   ~ t s *'  ' x t c $x{'X 0  ' < t C   ` static void MyAdd(Account a, int n) requires a.IsExposable; { a.Add(n); // Okay } StudentAccount s = new StudentAccount(); MyAdd(s, -1000); // But now here the requires clause fails P   =+   5 t  `G`H`I@VK#LM%N   7Statically bound: IsExposable property of Account frame8 8  t <Ě   J[Q] How to solve this? H t 0޽h ?t fp=___PPT10i.׈`+D='  = @B +] J 0 tl 4(  4~ 4 s *(ܚ 00   ~ 4 s *T   x 4 c $X 0   @ 4 C d  ` static void YourAdd(Account a, int n) { a.TryAdd(n); // OK! dynamically bound call } StudentAccount s = new StudentAccount(); YourAdd(s, -1000); [Q] How to verify modularily?P E  $   H 4 0޽h ? fp=___PPT10i.׈`+D='  = @B + J 0   p $G (  $~ $ s * 0   ~ $ s *  P   x $ c $PX     $ S     static void YourAdd(Account a, int n) requires a.IsDynamicExposable; { a.TryAdd(n); } StudentAccount s = new StudentAccount(); YourAdd(s, -1000);VP')A      $  f"GH_yIJ KLMN x p ,$D 0 ZIsDynamicExposable binds dynamically to the IsExposable property of the most derived frame[ [$ $v $  f(GHIJS K L}MN'  0,$D 0 BAt dynamic call sites, IsVirtualExposable means IsDynamicExposableC C,l @`   $@` ,$D 0Q  $ 6."`  YAt static call sites and when verifying the callee, IsVirtualExposable means IsExposableZ Z>- TB  $B c $D ` TB  $ c $D @@H $ 0޽h ?/ $$ fp=___PPT10p.׈`+J}D'  = @B D' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*$%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*$%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* $%(+p+0+$0 ++0+$0 +k L 0L0 jb )(  2 ' H\G7HXfPP }'enter expose ((StudentAccount) a) block( ( X2  0@@`x  0C"? @@X2  0P @@X2  0 @@p X2  0@@f   0"`@@PX2  0@@`f   0"`@@r  S c`P   X2  0P@@   0xe W#Account frame: owned, not exposable$ 2$   0j0P mStudentAccount frame: exposable 2 f  0"` @@ X2  0` @@ f  0"`p@@ X2  0@@  0o  LAccount frame: exposable 2  0|t P  kStudentAccount frame: exposed 2x  0C"?` @@ X2  0 @@   0x w  JAccount frame: exposed 2  0@} P kStudentAccount frame: exposed 2LB   c $D@@PLB ! c $D@@PLB " c $Dp@@ LB # c $Dp@@ LB $ c $D` @@LB % c $D` @@0 & 0  gStudentAccount object( 2 2 ( HG7HXf P`  T enter expose ((Account) a) block! !H  0޽h ? fp=___PPT10i.ۈ$+D='  = @B + L 0  t(  t~ t s *`P    t  6( "6 ?   H t 0޽h ? 33___PPT10i./p+D='  = @B + L 0 P(  r  S d`P     S <' <$@ 0  H  0޽h ? fp=___PPT10.>+EDZ'  = @B D' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*1%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*2V%(+ L 0 :(  r  S |`P   r  S \(      f (GbHIVJKAALM(CNF ` p  xD[Q] How does the static verifier know here that the invariant holds?E EH  0޽h ? fp=___PPT10i.>}+D='  = @B + L 0 f(  x  c $Ϝ`P   x  c $$3(   .   f\4(GjHQIJ KLMN  0 d[Q] Adding an ensures clause to this pure property getter would solve the problem. But is this okay?e eH  0޽h ? fp=___PPT10i.>}+D='  = @B + L 0 (  x  c $`P   x  c $O(   v   fHQ(GjHIJKLMNF ` 0 It turns out that in order to support state abstraction, it is sufficient to allow the declaration of private ensures clauses on pure methods.6 fN   fG(GdHYIWJ~K LwM N P` 0,$D 0 PBy default, these are derived from the body if the body is of the form return E;Q QH  0޽h ?/  fp=___PPT10.>}+ DO'  = @B D ' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(+8+0+0 + L 0 P \$(  \r \ S  `P   r \ S    H \ 0޽h ? fp=___PPT10i.r^+D='  = @B + L 0  x(  x~ x s */`P    x  6  "6 ?   H x 0޽h ? 33___PPT10i./p+D='  = @B + L 0 P `P(  `r ` S ,=`P    ` S ,> <$D 0  H ` 0޽h ? fp=___PPT10n.p>X+YDB'  = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*` %(+ L 0 |\(  |x | c $(`P  (  | c $( <$D 0 ( H | 0޽h ? fp=___PPT10n.p>X+YDB'  = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*| `%(+ L 0 p h0(  hx h c $l`P   x h c $`m   H h 0޽h ? fp=___PPT10i.p>X+D='  = @B + L 0 0(  x  c $u`P   x  c $v   H  0޽h ? fp=___PPT10i.p>X+D='  = @B + L 0 6(  ~  s *`P   x  c $  H  0޽h ? fp=___PPT10i.0"+D='  = @B + J 0  *(  x  c $, 0   r  S @  H  0޽h ? fp=___PPT10i.-)+D='  = @B + J 0  *(  x  c $ 0   r  S   H  0޽h ? fp=___PPT10i.+D='  = @B + J 0  |D(  |r | S ̱ 0    |  0"`   H | 0޽h ? fp=___PPT10i.G+D='  = @B +% 0 zr`  (  X  C    ?r  S ? 0  ? H  0޽h ? 3380___PPT10.@J& 0 zr  (  X  C    ?r  S ? 0  ? H  0޽h ? 3380___PPT10. 0 zr  (  X  C    Br  S $aB 0  B H  0޽h ? 3380___PPT10.Ѐf 0 zr0  (  X  C    Br  S uB 0  B H  0޽h ? 3380___PPT10.L=F 0 zr  (  X  C    Br  S B 0  B H  0޽h ? 3380___PPT10.P 0 zr  (  X  C    Cr  S C 0  C H  0޽h ? 3380___PPT10. H 0 zr  (  X  C    Gr  S $G 0  G H  0޽h ? 3380___PPT10.Po# 0 zr 8 (  8X 8 C    r 8 S @V 0   H 8 0޽h ? 3380___PPT10.PO 0 zr < (  <X < C    r < S _' 0   H < 0޽h ? 3380___PPT10.sk 0 zr @ (  @X @ C    r @ S  0   H @ 0޽h ? 3380___PPT10.@uo. 0 zr H (  HX H C    r H S h( 0   H H 0޽h ? 3380___PPT10.@_ 0 ~(  ^  S    Bx  c $B 0  B H  0޽h ? 3380___PPT10.L=` 0 ~0(  ^  S    Bx  c $DB 0  B H  0޽h ? 3380___PPT10.L=b 0 ~`(  ^  S    Bx  c $B 0  B H  0޽h ? 3380___PPT10.L=c 0 ~(  ^  S    Bx  c $B 0  B H  0޽h ? 3380___PPT10.L=e 0 ~(  ^  S    Cx  c $C 0  C H  0޽h ? 3380___PPT10. i 0 ~(  ^  S    Cx  c $C 0  C H  0޽h ? 3380___PPT10.Pm 0 ~`(  ^  S    Gx  c $G 0  G H  0޽h ? 3380___PPT10.Poo 0 ~(  ^  S    Ix  c $4G 0  I H  0޽h ? 3380___PPT10.Pou 0 ~(  ^  S    Cx  c $C 0  C H  0޽h ? 3380___PPT10.P 0 ~pl(  l^ l S    x l c $v 0   H l 0޽h ? 3380___PPT10.@uo 0 ~x(  x^ x S    x x c $<ޚ 0   H x 0޽h ? 3380___PPT10.@uo FxYkp>mYA8Ea)ck+`De#0b%d> vUvX,jEQ 2¾0)̓>7 n4?|Eu"*q,YˮǶe}a kͰY~-cl~*iu?}M Ѡ0/Ȗ<0G,Pz'qnBX7롯r%M?cOTi d'I ~+V,Dqb\6D cJ퐱kVQ? d/Hu5`:рXXXXhD,G@DB8NbBp>@܃фhhA"#B!"ˆbb=~D2v6"6!:dn2lE?`e)Y>;]Ṟ\ا |} uPf 0dm\dž?$k0P$3޼NHYf]zGjyurq;X6Ȇ.z{GSVOj[]d lS%3Jy+hh%זGLp'f3zZH<_4\vW9mmtT5 *z}mT'2)>zpiO_5%#`ZѽG]{f`#GRmFd#ki-˫>I̜,3?ѦL-_OYr:r+}Uòhl {k s,u$ ToCt@p ]IF=.Fw'((@?/9V azB8ϸ؂w-BS(㎈l ':r8e费-frّg:wƲ %.Ww_.dTÓW2Co1 l,}6-u- dۨ9pM>傺6f/D>)z.tL`\m=b؀)A8cQmnW%mxD=OD䜸n%IpK78aY,TDyc驎!%{ƷGs R…A|'r;pXi蘔g\! G "0FVe]1\ /G{rOQHq%AY"qb#{=u-tJzDz_2X~sI]4yÌr ~ѥ4nk'ٝh[E ?v](IY0yױZܝ~I.QqU%9VJ&wc>osv <䬭Q5 s. ;k#GOaF4|SA7"jΗW'f )OURɴF&%k@(;TegD*L+TQ2#NJJm^({49sj̪FteZhڗ4Ӡ㵲X]$<}"7Ljz^{zC{zBr;3E6dx&̚ծjeL>eX<ӛ͏Qc}5yB}_MFWߥ,%pAqT\#*?ڬ,frHCuQZ_Wt*ʓߡa۫R.SyFǷҥӥҥХN^WtͤIW.&]]L]>-|s)Fs)_tQZ_D|"76WQԿQ/zeGT!F`8~t ,A=nӍ~ows7HљD+x,؄ 3.)qҭS%>EeKlVhϘ8ͷp OOGIkQפoxm}[;{ cyx300YQ޶o/Cհ0d@$i!hl`v@/# xh\^m]Yf')϶&vn Q6o,.VT[VG $`v&==$ggȑǃx>gOH0 }C|Zu?%5V7Ho6ٗ g>=$z8[l7Nh9׳gwqi8zǏ*"ECPe嗋-y-„-/H[*F#-'0{(r9Ok9Ƒ;?.ÿ=UޑS']v+U@Eˠg)sOk w?1t)8gz'?skٱO_g'g ~zؐ'Byy~5kB  ^!$C~!¢x./^?_@aAbBbCbDbEaG`H_J^L]N\P\T]X^\_aaebjcndreudxc{b~a_^]\--'--$ -)! "(----'--$ &)-,'"  --'--$ !"%  --'--$('&(()(--'--6$ "(-/*('(,(#$&#!!   --'--$ &# --'--$    --'--"$      --'-- %034567788899::--'@BComic Sans MS-. 2 (8 The Spec# .-@BComic Sans MS-. %2 4 Programming System: .-@BComic Sans MS-. 2 ?4 An Overview .-@BComic Sans MS-. 2 )8 The Spec# .. 2 (7 The Spec# .-@BComic Sans MS-. %2 5 Programming System: .. %2 4Programming System: .-@BComic Sans MS-. 2 @4 An Overview .. 2 ?3 An Overview .-@BComic Sans MS-. "2 L?Tutor: Bart Jacobs.. "2 K>Tutor: Bart Jacobs.-@BComic Sans MS-. 2 Q0PhD student at .. 2 P/PhD student at .-@BComic Sans MS-. 2 QM K.U.Leuven.. 2 PL K.U.Leuven.-@BComic Sans MS-. 2 Q` , Belgiumn.. 2 P_ , Belgiumn.-@BComic Sans MS-. !2 W@Spec# contributors.. !2 V?Spec# contributors.-IR5WEC5VRTQ==2 EYEYItem 5Properties7 ?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~     !"#$%&'()*+./0123D56789:;BC,EOPQRSTFRoot EntrydO)EYNCurrent User4SummaryInformation( PowerPoint Document(1?DocumentSummaryInformation8  MsoDataStore EYEYZZNY1O0HQ==2EYEYItem PropertiesXKDQUO43ED==2 EYEYItem  -Propertieskeywords" minOccurs="0" maxOccurs="1" type="xsd:string"/> This value indicates the number of saves or revisions. The application is responsible for updating this value after each revision. d:all> d:complexType> This value indicates the number of saves or revisions. The application is responsible for updating this value after each revision.   !"#$%&'()*+,-./01234689:DocumentLibraryFormDocumentLibraryFormDocumentLibraryForm w> ՜.+,D՜.+,     vOn-screen Show1?%O UArialComic Sans MSEras Demi ITC WingdingsCrayons 1_Crayons*The Spec# Programming System: An OverviewWhat is Spec#? Spec# GoalsDemo: The Bag Class Tutorial TutorialNon-null typesTypes versus Assertions"Non-null types are flow-sensitive$Non-null Fields and Object CreationNon-nullness of FieldsNon-nullness of PropertiesFields and Properties TutorialPreconditionsChecked ExceptionsDefinedness of contracts TutorialFrom Spec#...via BoogiePL via BoogiePL-DSA via Passive BoogiePL  without contracts  without contracts to Logic TutorialObject InvariantsObject Invariants Re-entrancy Re-entrancy#Spec# Object Invariant MethodologyExposing objectsExposing objectsObject Invariants: Example&Object Invariants and Object CreationObject Invariants: RecapInvariants and ExceptionsInvariants and Exceptions TutorialInter-object InvariantsInter-object InvariantsInter-object InvariantsUpdating Owned ObjectsObject LifecycleObject LifecycleObject LifecycleObject LifecycleObject LifecycleObject LifecycleObject LifecycleObject LifecycleObject LifecycleObject Lifecycle IsExposableOwnership System Tutorial SubclassingSubclassing as ContainmentSubclassing as ContainmentLearning from Containment SubclassingVirtual methods$Modular verification of inheritance Inheritance Tutorial Pure MethodsState AbstractionState AbstractionState Abstraction!State Abstraction and Interfaces TutorialMultithreadingMultithreadingMultithreadingMultithreadingMultithreadingReaders-WritersWait Conditions Thank You!  Fonts UsedDesign Template Slide TitlesO0VersionPublishingExpirationDatePublishingStartDate2018-12-08T06:59:54Z2000-01-01T00:00:00Z