Theory WP

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory WP
imports Main
begin

definition
  triple_judgement :: "('a ⇒ bool) ⇒ 'b ⇒ ('a ⇒ 'b ⇒ bool) ⇒ bool"
where
 "triple_judgement pre body property = (∀s. pre s ⟶ property s body)"

definition
  postcondition :: "('r ⇒ 's ⇒ bool) ⇒ ('a ⇒ 'b ⇒ ('r × 's) set)
            ⇒ 'a ⇒ 'b ⇒ bool"
where
 "postcondition P f = (λa b. ∀(rv, s) ∈ f a b. P rv s)"

definition
  postconditions :: "('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool)"
where
 "postconditions P Q = (λa b. P a b ∧ Q a b)"

ML_file ‹WP-method.ML›

declare [[wp_warn_unused = false]]

setup WeakestPre.setup

method_setup wp = ‹WeakestPre.apply_rules_args false›
  "applies weakest precondition rules"

method_setup wp_once = ‹WeakestPre.apply_once_args false›
  "applies one weakest precondition rule"

method_setup wp_trace = ‹WeakestPre.apply_rules_args true›
  "applies weakest precondition rules with tracing"

method_setup wp_once_trace = ‹WeakestPre.apply_once_args true›
  "applies one weakest precondition rule with tracing"

end