Dafny is an experimental language that explores the dynamic frames style of specifications in an object-based sequential setting.