Abstract

Vision

  • Increased programmer productivity and program reliability through increased rigor
  • Record design decisions
  • + Utilize automatic checking
  • = Detect errors and improve maintainability