RefactorIntroduction

Introduction

to Refactoring Java Contracts

Java Contracts

• Representation of JML using Java code by Patrice Chalin & Robby
• Reuses JML 5 Annotations by Kristina Taylor
• Inspired by Code Contracts in .net, by Microsoft

Java Contract Types

• Method based - java methods used to encode the specification.
  • Invariants
  • Model Fields
• Statement based - java statement used to encode the specification.
  • Preconditions
  • Postconditions
• Block Based - java statement followed by a java block.
  • SpecCase?

Refactoring Operations

• Pull Up
  • Select for Super type to pull up to.
  • Ensure destination method exists for Statement refactorings
  • Ensure all code require for the contract is available in destination type
• Push Down
  • Select for Sub type to push down to.
  • Ensure destination method exists for Statement refactorings
  • Ensure all code require for the contract is available in destination type

Refactoring Plugin