KeY-1.4.0 (2009-03-25)

• Unified proof obligation framework
  • sharing of proof obligations across different specification languages
  • unified API for adding new proof obligations
  • same GUI elements used for all specification languages
  • more elegant translation of \old, @pre-like constructs
• Improved JavaCard DL Specification interface
  • specification of DL invariants
• Rewrite of JML front-end
  • ghost variables/fields and JML set statement
  • non_null by default
  • \old in loop invariants supported
  • \object_creation(type) in JML assignable clauses
• New standalone OCL front-end
  • discontinued support for Borland Together integration
• Java language support enhancements:
  • enum types (partially)
  • inner and anonymous classes
  • enhanced for loop
  • variable method arguments
  • covariant method signature
• Generation of JML specifications
• Strictly pure queries can be pushed directly into an update
• Stable proof loading and saving
• Classpath directive
• various bugfixes