(* Author: Tobias Nipkow *)
theory Abs_Int0
imports Abs_Int_init
begin
subsection "Orderings"
text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class top} are
defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}.
If you view this theory with jedit, just click on the names to get there. *}
class semilattice = semilattice_sup + top
instance "fun" :: (type, semilattice) semilattice ..
instantiation option :: (order)order
begin
fun less_eq_option where
"Some x \<le> Some y = (x \<le> y)" |
"None \<le> y = True" |
"Some _ \<le> None = False"
definition less_option where "x < (y::'a option) = (x \<le> y \<and> \<not> y \<le> x)"
lemma le_None[simp]: "(x \<le> None) = (x = None)"
by (cases x) simp_all
lemma Some_le[simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
by (cases u) auto
instance proof
case goal1 show ?case by(rule less_option_def)
next
case goal2 show ?case by(cases x, simp_all)
next
case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, auto)
next
case goal4 thus ?case by(cases y, simp, cases x, auto)
qed
end
instantiation option :: (sup)sup
begin
fun sup_option where
"Some x \<squnion> Some y = Some(x \<squnion> y)" |
"None \<squnion> y = y" |
"x \<squnion> None = x"
lemma sup_None2[simp]: "x \<squnion> None = x"
by (cases x) simp_all
instance ..
end
instantiation option :: (semilattice)semilattice
begin
definition top_option where "\<top> = Some \<top>"
instance proof
case goal4 show ?case by(cases a, simp_all add: top_option_def)
next
case goal1 thus ?case by(cases x, simp, cases y, simp_all)
next
case goal2 thus ?case by(cases y, simp, cases x, simp_all)
next
case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
qed
end
lemma [simp]: "(Some x < Some y) = (x < y)"
by(auto simp: less_le)
instantiation option :: (order)bot
begin
definition bot_option :: "'a option" where
"\<bottom> = None"
instance
proof
case goal1 thus ?case by(auto simp: bot_option_def)
qed
end
definition bot :: "com \<Rightarrow> 'a option acom" where
"bot c = anno None c"
lemma bot_least: "strip C = c \<Longrightarrow> bot c \<le> C"
by(induct C arbitrary: c)(auto simp: bot_def)
lemma strip_bot[simp]: "strip(bot c) = c"
by(simp add: bot_def)
subsubsection "Pre-fixpoint iteration"
definition pfp :: "(('a::order) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
"pfp f = while_option (\<lambda>x. \<not> f x \<le> x) f"
lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<le> x"
using while_option_stop[OF assms[simplified pfp_def]] by simp
lemma while_least:
fixes q :: "'a::order"
assumes "\<forall>x\<in>L.\<forall>y\<in>L. x \<le> y \<longrightarrow> f x \<le> f y" and "\<forall>x. x \<in> L \<longrightarrow> f x \<in> L"
and "\<forall>x \<in> L. b \<le> x" and "b \<in> L" and "f q \<le> q" and "q \<in> L"
and "while_option P f b = Some p"
shows "p \<le> q"
using while_option_rule[OF _ assms(7)[unfolded pfp_def],
where P = "%x. x \<in> L \<and> x \<le> q"]
by (metis assms(1-6) order_trans)
lemma pfp_bot_least:
assumes "\<forall>x\<in>{C. strip C = c}.\<forall>y\<in>{C. strip C = c}. x \<le> y \<longrightarrow> f x \<le> f y"
and "\<forall>C. C \<in> {C. strip C = c} \<longrightarrow> f C \<in> {C. strip C = c}"
and "f C' \<le> C'" "strip C' = c" "pfp f (bot c) = Some C"
shows "C \<le> C'"
by(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(5)[unfolded pfp_def]])
(simp_all add: assms(4) bot_least)
lemma pfp_inv:
"pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y"
unfolding pfp_def by (metis (lifting) while_option_rule)
lemma strip_pfp:
assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"
using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp
subsection "Abstract Interpretation"
definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}"
fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
"\<gamma>_option \<gamma> None = {}" |
"\<gamma>_option \<gamma> (Some a) = \<gamma> a"
text{* The interface for abstract values: *}
locale Val_abs =
fixes \<gamma> :: "'av::semilattice \<Rightarrow> val set"
assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
fixes num' :: "val \<Rightarrow> 'av"
and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
assumes gamma_num': "i \<in> \<gamma>(num' i)"
and gamma_plus': "i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1+i2 \<in> \<gamma>(plus' a1 a2)"
type_synonym 'av st = "(vname \<Rightarrow> 'av)"
locale Abs_Int_fun = Val_abs \<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
begin
fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
"aval' (N i) S = num' i" |
"aval' (V x) S = S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
definition "fa x e S = (case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S)))"
definition "step' = Step fa (\<lambda>b S. S)"
lemma strip_step'[simp]: "strip(step' S C) = strip C"
by(simp add: step'_def)
definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI c = pfp (step' \<top>) (bot c)"
abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
where "\<gamma>\<^isub>s == \<gamma>_fun \<gamma>"
abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>s"
abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s \<top> = UNIV"
by(simp add: top_fun_def \<gamma>_fun_def)
lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o \<top> = UNIV"
by (simp add: top_option_def)
lemma mono_gamma_s: "f1 \<le> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
lemma mono_gamma_o:
"S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
text{* Soundness: *}
lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def)
lemma in_gamma_update: "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
by(simp add: \<gamma>_fun_def)
lemma gamma_Step_subcomm:
assumes "!!x e S. f1 x e (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (f2 x e S)" "!!b S. g1 b (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (g2 b S)"
shows "Step f1 g1 (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (Step f2 g2 S C)"
proof(induction C arbitrary: S)
qed (auto simp: mono_gamma_o assms)
lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
(auto simp: aval'_sound in_gamma_update fa_def split: option.splits)
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
proof(simp add: CS_def AI_def)
assume 1: "pfp (step' \<top>) (bot c) = Some C"
have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C" --"transfer the pfp'"
proof(rule order_trans)
show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
show "... \<le> \<gamma>\<^isub>c C" by (metis mono_gamma_c[OF pfp'])
qed
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
qed
end
subsubsection "Monotonicity"
lemma mono_post: "C1 \<le> C2 \<Longrightarrow> post C1 \<le> post C2"
by(induction C1 C2 rule: less_eq_acom.induct) (auto)
locale Abs_Int_fun_mono = Abs_Int_fun +
assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
begin
lemma mono_aval': "S \<le> S' \<Longrightarrow> aval' e S \<le> aval' e S'"
by(induction e)(auto simp: le_fun_def mono_plus')
lemma mono_update: "a \<le> a' \<Longrightarrow> S \<le> S' \<Longrightarrow> S(x := a) \<le> S'(x := a')"
by(simp add: le_fun_def)
lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
unfolding step'_def
by(rule mono2_Step)
(auto simp: mono_update mono_aval' fa_def split: option.split)
lemma mono_step'_top: "C \<le> C' \<Longrightarrow> step' \<top> C \<le> step' \<top> C'"
by (metis mono_step' order_refl)
lemma AI_least_pfp: assumes "AI c = Some C" "step' \<top> C' \<le> C'" "strip C' = c"
shows "C \<le> C'"
by(rule pfp_bot_least[OF _ _ assms(2,3) assms(1)[unfolded AI_def]])
(simp_all add: mono_step'_top)
end
instantiation acom :: (type) vars
begin
definition "vars_acom = vars o strip"
instance ..
end
lemma finite_Cvars: "finite(vars(C::'a acom))"
by(simp add: vars_acom_def)
subsubsection "Termination"
lemma pfp_termination:
fixes x0 :: "'a::order" and m :: "'a \<Rightarrow> nat"
assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x < y \<Longrightarrow> m x > m y"
and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<le> f x0"
shows "\<exists>x. pfp f x0 = Some x"
proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<le> f x"])
show "wf {(y,x). ((I x \<and> x \<le> f x) \<and> \<not> f x \<le> x) \<and> y = f x}"
by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
next
show "I x0 \<and> x0 \<le> f x0" using `I x0` `x0 \<le> f x0` by blast
next
fix x assume "I x \<and> x \<le> f x" thus "I(f x) \<and> f x \<le> f(f x)"
by (blast intro: I mono)
qed
locale Measure1_fun =
fixes m :: "'av::{order,top} \<Rightarrow> nat"
fixes h :: "nat"
assumes h: "m x \<le> h"
begin
definition m_s :: "vname set \<Rightarrow> 'av st \<Rightarrow> nat" ("m\<^isub>s") where
"m_s X S = (\<Sum> x \<in> X. m(S x))"
lemma m_s_h: "finite X \<Longrightarrow> m_s X S \<le> h * card X"
by(simp add: m_s_def) (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
definition m_o :: "vname set \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
"m_o X opt = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s X S)"
lemma m_o_h: "finite X \<Longrightarrow> m_o X opt \<le> (h*card X + 1)"
by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
"m_c C = (\<Sum>i<size(annos C). m_o (vars C) (annos C ! i))"
text{* Upper complexity bound: *}
lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
proof-
let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))" by(simp add: m_c_def)
also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
also have "\<dots> = ?a * (h * ?n + 1)" by simp
finally show ?thesis .
qed
end
lemma le_iff_le_annos_zip: "C1 \<le> C2 \<longleftrightarrow>
(\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<le> a2) \<and> strip C1 = strip C2"
by(induct C1 C2 rule: less_eq_acom.induct) (auto simp: size_annos_same2)
lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
text{* The predicates @{text "top_on_ty X a"} that follow describe that @{text a} is some object
that maps all variables in @{text X} to @{term \<top>}.
This is an important invariant for the termination proof where we argue that only
the finitely many variables in the program change. That the others do not change
follows because they remain @{term \<top>}. *}
fun top_on_st :: "vname set \<Rightarrow> 'a::top st \<Rightarrow> bool" where
"top_on_st X f = (\<forall>x\<in>X. f x = \<top>)"
fun top_on_opt :: "vname set \<Rightarrow> 'a::top st option \<Rightarrow> bool" where
"top_on_opt X (Some F) = top_on_st X F" |
"top_on_opt X None = True"
definition top_on_acom :: "vname set \<Rightarrow> 'a::top st option acom \<Rightarrow> bool" where
"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on_opt X a)"
lemma top_on_top: "top_on_opt X (\<top>::_ st option)"
by(auto simp: top_option_def)
lemma top_on_bot: "top_on_acom X (bot c)"
by(auto simp add: top_on_acom_def bot_def)
lemma top_on_post: "top_on_acom X C \<Longrightarrow> top_on_opt X (post C)"
by(simp add: top_on_acom_def post_in_annos)
lemma top_on_acom_simps:
"top_on_acom X (SKIP {Q}) = top_on_opt X Q"
"top_on_acom X (x ::= e {Q}) = top_on_opt X Q"
"top_on_acom X (C1;C2) = (top_on_acom X C1 \<and> top_on_acom X C2)"
"top_on_acom X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
(top_on_opt X P1 \<and> top_on_acom X C1 \<and> top_on_opt X P2 \<and> top_on_acom X C2 \<and> top_on_opt X Q)"
"top_on_acom X ({I} WHILE b DO {P} C {Q}) =
(top_on_opt X I \<and> top_on_acom X C \<and> top_on_opt X P \<and> top_on_opt X Q)"
by(auto simp add: top_on_acom_def)
lemma top_on_sup:
"top_on_opt X o1 \<Longrightarrow> top_on_opt X o2 \<Longrightarrow> top_on_opt X (o1 \<squnion> o2 :: _ st option)"
apply(induction o1 o2 rule: sup_option.induct)
apply(auto)
done
lemma top_on_Step: fixes C :: "('a::semilattice)st option acom"
assumes "!!x e S. \<lbrakk>top_on_opt X S; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt X (f x e S)"
"!!b S. top_on_opt X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt X (g b S)"
shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt X S; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (Step f g S C)"
proof(induction C arbitrary: S)
qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
locale Measure_fun = Measure1_fun +
assumes m2: "x < y \<Longrightarrow> m x > m y"
begin
lemma m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
by(auto simp: le_less m2)
lemma m_s2_rep: assumes "finite(X)" and "S1 = S2 on -X" and "\<forall>x. S1 x \<le> S2 x" and "S1 \<noteq> S2"
shows "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
proof-
from assms(3) have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S2 x)" by (simp add: m1)
from assms(2,3,4) have "EX x:X. S1 x < S2 x"
by(simp add: fun_eq_iff) (metis Compl_iff le_neq_trans)
hence 2: "\<exists>x\<in>X. m(S1 x) > m(S2 x)" by (metis m2)
from setsum_strict_mono_ex1[OF `finite X` 1 2]
show "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))" .
qed
lemma m_s2: "finite(X) \<Longrightarrow> S1 = S2 on -X \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s X S1 > m_s X S2"
apply(auto simp add: less_fun_def m_s_def)
apply(simp add: m_s2_rep le_fun_def)
done
lemma m_o2: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
proof(induction o1 o2 rule: less_eq_option.induct)
case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
next
case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h)
next
case 3 thus ?case by (auto simp: less_option_def)
qed
lemma m_o1: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
by(auto simp: le_less m_o2)
lemma m_c2: "top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2 \<Longrightarrow>
C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
let ?X = "vars(strip C2)"
assume top: "top_on_acom (- vars(strip C2)) C1" "top_on_acom (- vars(strip C2)) C2"
and strip_eq: "strip C1 = strip C2"
and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
by (metis (lifting, no_types) finite_cvars m_o1 size_annos_same2)
fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
have topo1: "top_on_opt (- ?X) (annos C1 ! i)"
using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
have topo2: "top_on_opt (- ?X) (annos C2 ! i)"
using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
show "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
< (\<Sum>i<size(annos C2). m_o ?X (annos C1 ! i))"
apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
qed
end
locale Abs_Int_fun_measure =
Abs_Int_fun_mono where \<gamma>=\<gamma> + Measure_fun where m=m
for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
begin
lemma top_on_step': "\<lbrakk> vars C \<subseteq> -X; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (step' \<top> C)"
unfolding step'_def
by(rule top_on_Step)
(auto simp add: top_option_def fa_def split: option.splits)
lemma AI_Some_measure: "\<exists>C. AI c = Some C"
unfolding AI_def
apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on_acom (- vars C) C" and m="m_c"])
apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
apply(auto simp add: top_on_step' vars_acom_def)
done
end
text{* Problem: not executable because of the comparison of abstract states,
i.e. functions, in the post-fixedpoint computation. *}
end