Object-Oriented Programming

Class definition

  class ClassName {}

  predicate IsObject(c: ClassName) { c is object }

  predicate IsRef(c: ClassName?) { c is object? }

• The class declaration gives rise to two types:
  • ClassName is the type of references to ClassName objects
  • ClassName? additionally contains the value null
• object is the type of all references
• object? additionally contains the value null

Generic class definition

  class ClassName<T> {}

• A class definition can be parameterized by other types

Mutable fields

  class C<T(0)> {

    var mutableField: T

  }

• Dafny does not have information hiding modifiers (private, protected, …)
  • (Hiding is done via module export sets)
• We see our second type characteristic: auto-init (0)
  • Type characteristic 0 says that variables of the type can be auto-initialized
  • Corresponding type arguments must come with a way to choose some value at run time
• Auto-init types
  • All built-in types are auto-init
  • Possibly-null reference types are auto-init
  • A datatype instantiated with auto-init type arguments is auto-init

New functional expressions

  predicate MemberAccess<T(0)>(c: C) { c.mutableField is T }

New RHS expressions

  method Allocate<T(0)>() returns (c: C) {
    c := new C;
  }

• Once allocated, all the object's fields are auto-initialized
• To arbitrary values of their types

New $\ell$-values

  method Update<T(0)>(c: C, value: T) {
    c.mutableField := value;
  }

• Side effect
• Updates the value of field mutableField of the object referenced by c

Immutable fields

  class C {

    const immutableField: int := 4

  }

New functional expression: this

  class C {

    var mutableField: int

    predicate This() { this is C }

  }

• Self reference to the object
• Member-access expressions can omit “this.” (if there are no name conflicts)
  • For example, this.mutableField can be written simply as mutableField

Constructors

  class C {

    var mutableField: int
    const immutableField: int

    constructor (i: int, j: int) {
      immutableField := i;
      mutableField := j;
    }

  }

  method M() {
    var c := new C(3, 4);
  }

• A class can provide a custom constructors
• One constructor can be unnamed (the anonymous constructor)
• Constant fields can be initialized in constructor bodies
• When a class has a constructor, some constructor must be called as part of new

Multiple constructors

  class C {

    var mutableField: int
    const immutableField: int

    constructor Partial(i: int) {
      immutableField := i;
    }

    constructor FromStringLength(s: string) {
      mutableField := 0;
      immutableField := |s|;
    }

    method M() {
      var c := new C.FromStringLength("abc");
    }

  }

Two-phase construction

  class C {

    var mutableField: int
    const immutableField: int

    constructor(i: int, j: int) {
      immutableField := i;
      new;
      mutableField := j;
    }

  }

• new; divides the two phases of the constructor
• If new; is omitted, the first phase is the entire constructor body and the second phase is empty
• After new;, the object is considered allocated
• The first phase restricts the use of this
• Constant fields can be set only in the first phase

Other member declarations/definitions

  class C {

    var mutableField: int

    method Print() {
      print mutableField, "\n";
    }

    function Get(): int {
      mutableField
    }

  }

• Methods and functions can be members of a class definition
• Types are not allowed as members
  • No lexically nested type declarations

Traits

  trait TraitName { }

• A trait is an abstract supertype of other types
• Traits can be defined in the same way as classes
• Unlike classes, traits cannot be instantiated and have no constuctors

Inheritance

  trait T {
    method Print() { print("Hello, World!"); }
  }

  class C extends T {
    method RePrint() { Print(); }
  }

• A type (trait, class, datatype, opaque type) can inherit from (that is, extend, or implement) any number of traits
• Nothing can inherit from a class
• A type is allowed to inherit a trait more than once, but only if each time is with the same type-parameter instantiation

Subtyping

  trait A {
    method Print() { print("Hello, World!"); }
  }

  trait B extends A {}
  
  method M1(o: A) { o.Print(); }
  
  method M2(o: B) { M1(o); }

• Subtyping is nominal

Late binding

  trait T {

    function G(x: int): int
    
    function F(x: int): int { G(x) }

  }

  class C extends T {
    
    function G(x: int): int { x + 1 }
  
  }

• A member declaration in a trait can be left undefined
• Member declarations are eventually defined in the class
• The use of a declaration is late bound to that definition

Overriding

• As a first approximation
  • A declaration can override another declaration
  • A definition can override a declaration
  • A definition can never override a definition

Encapsulation

  trait Complex {
    function Real(): real
    function Im(): real
  }

  class PolarComplex extends Complex {
  
    var r: real
    var i: real
  
    function Real(): real { r }
    function Im(): real { r }
  
  }

• Information hiding achieved through traits

Dynamic dispatch

  trait Printer {
    method Print()
  }
  class A extends Printer {
    method Print() { print("A\n"); }
  }
  class B extends Printer {
    method Print() { print("B\n"); }
  }

  method Print(p: Printer) {
    p.Print();
  }

  method Main() {

    var a := new A;
    var b := new B;
    Print(a);
    Print(b);

  }

Conclusion

• Dafny's OO system has been carefully designed
• Object initialization is flexibly controlled by two-phase constructors
• Restrictions on overriding are stronger that in most other OO languages
• Semantics is simpler