Correctness.scala

trait Correctness {
  
  // Let’s talk about programs.
  type P
  
  // A specification is a predicate on a program.
  trait S { def apply (p: P): Boolean }
  
  // We say "p implements s" when a program meets a specification.
  def `p implements s` (p: P, s: S) = s (p)
  
  // We shorten this to "p is correct" when a specification is contextually impli…