Email Gateway (Jun 28 2022 at 17:07): Email Gateway (Jun 28 2022 at 17:07):From: Valentin Springsklee <uidpn@student.kit.edu>
Hello,
I want to proof total correctness of a monadic program using the
Isabelle Refinement Framework.
I have a program that iterates over a list an and computes a conditional
sum. I have already shown partial correctness relative to the
specification and used the Isabelle code generation. I used
theRefine_Monadic_Userguide as a reference
(https://www.isa-afp.org/browser_info/current/AFP/Collections/Refine_Monadic_Userguide.html)
My function looks like this. The While loop iterates over p, a list if
Relations and accumulates the entries that fulfill that a is the top of
the relation.
definition "wc_spec p a = SPEC (λac. ac = card {i::nat. i < length p ∧
above (p!i) a = {a}})"
definition "wc_invar p0 a ≡ λ(r,ac).
r ≤ length p0
∧ ac = card{i::nat. i < r ∧ above (p0!i) a = {a}}"
definition win_count_mon :: "'a Profile ⇒ 'a ⇒ nat nres" where
"win_count_mon p a ≡ do {
(r, ac) ← WHILEI/T (wc_invar p a) (λ(r, _). r < length p) (λ(r, ac). do {
ASSERT (r < length p);
let ac = ac + (if (above (p!r) a = {a}) then 1 else 0);
RETURN (r + 1, ac)
})(0,0);
RETURN ac
}"
I believe that in order to show total correctness, I need to use the
variant that (length p - r) decreases for each iteration. Do I also have
to provide that p is finite? The WHILET Rule with refine_vcg opens a
goal to prove well-foundedness of some relation. How do I instantiate it
with the appropriate variant of the while loop?
I hope, my question is somewhat understandable. I am happy to clarify
and provide further information.
Thank you,
Valentin Springsklee
Last updated: Jul 15 2022 at 23:21 UTC