Sumários

Dafny: DbC and Classes

8 Novembro 2023, 18:30 • Antónia Lopes

Design by contract : Contracts for Data Abstractions

8 Novembro 2023, 16:30 • Antónia Lopes

  • Design by contract: Contracts for Data Abstractions (cont'd)
    • Model-based specifications
      • Abstraction functions
      • Using existing Immutable Types as models
    • Model-based specifications for Object Types
    • Model-based specifications for Immutable Types 
      • Inductive datatypes
    • Brief overview of design by contract in Java with JML

Exercises about DbC applied to procedures and classes

25 Outubro 2023, 18:30 • Antónia Lopes

  • Exercises3 (Dafny&DbC): 5, 6, 7, 9
  • Exercises4 (Dafny&Classes): 1 

Design by contract: Contracts for Data Abstractions

25 Outubro 2023, 16:30 • Antónia Lopes

  • Design by contract: Contracts for Procedural Abstractions (cont'd)
    • Additional types: arrays, matrices and sequences 
    • Additional specification primitives: quantifiers, read and write frames, old, fresh predicate
    • Examples: linear search in an array, grow array, copy array
  • Classes in Dafny
  • Design by contract: Contracts for Data Abstractions
    • Invariants and representation invariants
    • Property-based specifications

Exercises Mechanised Proofs with Dafny

18 Outubro 2023, 18:30 • Antónia Lopes

  • Exercises2 (Dafny-Hoare): 2,3, 8