Verifying Abstractions in Model Checking ---------------------------------------- (Safety Lemma for the prefix Operation) ------ Summary: Generalisation(?) Lemmas Challenges for Rippling ------ Definitions: aelem ----- enumerated type containing elements {e1, e2, ne} order ----- enumerated type containing elements {eps1, e1l, e2l, e1e2l, e2e1l, error} alist ----- New Type quad(bool, bool, aelem, order) A quadruple of two booleans an aelem and an order (forming the abstraction of a listof naturals) The first boolean indicates whether the list is empty, the second whether it has only one element. alphaelem --------- nat -> aelem alphaelem(2) = e1 alphaelem(5) = e2 (not (N = 2) or (N = 5)) -> alphaelem(N) = ne combine ------- (aelem, order) -> order combine(ne, X) = X combine(e1, eps1) = el1 combine(e1, e2l) = e1e21 combine(e2, eps1) = e2l combine(e2, e1l) = e2e1l (not (X = eps1) or (X = e21)) -> combine(e1, X) = error (not (X = eps1) or (X = e11)) -> combine(e2, X) = error alphaorder ---------- list -> order alphaorder(nil) = eps1 alphaorder(h::t) = combine(alphaelem(h), alphaorder(t)) alpha ----- list -> alist alpha(nil) = quad(false, false, ne, eps1) alpha(x::nil) = quad(true, true, alphaelem(x), eps1) alpha(h1::h2::t) = quad(true, false, alphaelem(h1), alphaorder(h2::t)) prefix ------ (list, list) -> bool prefix(nil, L) = true prefix(h::t1, h::t2) = prefix(t1, t2) (not (h1 = h2)) -> prefex(h1::t1, h2::t2) = false aprefix ------- (alist, alist) -> bool aprefix(quad(false, A, B, C), quad(E, F, G, H)) = true aprefix(quad(A, B, C, D), quad(E, F, G, error)) = true aprefix(quad(A, true, D, eps1), quad(true, F, G, H)) = true aprefix(quad(A, B, D, eps1), quad(true, false, G, H)) = true aprefix(quad(A, true, D, e11), quad(E, F, G, e1l)) = true aprefix(quad(A, B, D, e11), quad(E, false, G, e1l)) = true aprefix(quad(A, true, D, e11), quad(E, F, G, e1e2l)) = true aprefix(quad(A, B, D, e21), quad(E, false, G, e2l)) = true aprefix(quad(A, B, D, e21), quad(E, F, G, e2e1l)) = true otherwise false ------ Theorem: forall l1, l2: list prefix(l1, l2) -> aprefix(alpha(l1), alpha(l2)) ------ Comments: Provided by Dieter Hutter for 2000 Challenges. The presentation above has been altered from Dieter's for no good reason except to provide some kind of consistency of presentation. Believe the problems involve the need for generalisations and some challenges for Rippling. Lemmas required by INKA include: aprefix(quad(true, false, U, Y), quad(true, false, V, Z)) -> aprefix(quad(true, false, W, combine(X, Y)), quad(trye, false, W, combine(X, Z))) aprefix(quad(true, false, U, combine(U, eps1)), quad(true, false, U, combine(U, V))) prefix(Y, Z) -> aprefix(quad(true, false, Z, alphaorder(Y)), quad(ture, false, X, alphaorder(Z))) ------ Dieter's Presentation: Problem: Verifying Abstractions in Model Checking Contact: Dieter Hutter Date: 4/28/2000 (revised 6/7/2000) ================================================================= Many thanks to Dennis Dams (Eindhoven University) who provided this challenge. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% structure nil, cons(car:nat, cdr:list):list; structure tt,ff:bool; % Our own version of the booleans, used in a limited way. enum structure tt, ff : bool; function mynot(b:bool):bool = if b = tt then ff % if b = ff then tt; % % % The abstract side. % For a natural number, the only information we are interested in is whether % it's p2, p5, or something else. % % Abbreviations for some positive numbers. function p2:nat = s(s(0)); function p5:nat = s(s(s(p2))); % % Abstraction for the naturals. The idea is that e1 represents p2, % e2 represents p5, and ne represents any other number (ne is also % used to represent "nothing" in case of abstracting the head of an % empty list. We'll refer to % a natural that abstracts into e1 as an "e1-element", and a natural % that abstracts into e2 as an "e2-element". enum structure e1, e2, ne : aelem; % The abstraction of naturals is captured by the function alphaelem. function alphaelem(a:nat):aelem = if a = p2 then e1 otherwise { if a = p5 then e2 otherwise ne}; % Abstraction of lists over naturals, based on the above abstraction of % individual naturals. Basically, the abstraction of a list says whether % there are occurences of e1-elements and e2-elements, if so, in which % order they occur, and whether there are multiple e1 or e2 elements. In % addition, the information whether the list is empty, whether it has % exactly one element, and what is the abstraction of its head is % maintained. More precisely, an abstract list is a quadruple % quad(nonempty:bool, oneelem:bool, hd:aelem, ord:order), where nonempty % tells us whether the list is nonempty, oneelem whether it has exactly % one element, and hd is the abstraction of the head. The last field, % ord, basically gives information about the occurrence and order of % e1-elements and e2-elements in the list. In the case that there are % multiple occurrences of e1 or e2 in the list, then this is represented % by the ord field having value error. enum structure epsl, e1l, e2l, e1e2l, e2e1l, error : order; structure quad(nonempty:bool, oneelem:bool, hd:aelem, ord:order) : alist; % The following auxiliary functions will be used for computing the % abstraction of a list by function alpha below. function check_nonempty(l:list):bool = if l = nil then ff otherwise tt; function hasoneelem(l:list):bool = if l = nil then ff otherwise{ if cdr(l) = nil then tt otherwise ff}; function combine(x:aelem, y:order):order = if x = ne then y if x = e1 and y = epsl then e1l if x = e1 and y = e2l then e1e2l if x = e2 and y = epsl then e2l if x = e2 and y = e1l then e2e1l otherwise error; function alphaorder(l:list):order = if l = nil then epsl otherwise combine(alphaelem(car(l)), alphaorder(cdr(l))); % Now we can define the function alpha that abstracts a concrete list. % Uses a hack: when taking the car of an empty list, INKA seems to % always return the "first" value of the element type. So the car of % an empty list over nat is 0. This fact is used in calculating the % 3rd field. Note that this is wrong when 0 is a distinguished element % (e1-element). function alpha(l:list):alist = quad(check_nonempty(l), hasoneelem(l), alphaelem(car(l)), alphaorder(l)); ;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % prefix(l1,l2) checks whether l1 is a prefix of l2. function prefix(l1,l2:list):bool = if l1 = nil then tt if l1 of cons then { if car(l1) = car(l2) then prefix(cdr(l1), cdr(l2)) otherwise ff }; % The abstract prefix relation and the corresponding safety lemma. function aprefix(l1:alist, l2:alist):bool = if nonempty(l1) = ff then tt otherwise {if tl(l2) = error then tt otherwise {if tl(l1) = epsl AND nonempty(l2) = tt AND oneelem(l1) = tt then tt otherwise {if tl(l1) = epsl AND nonempty(l2) = tt AND oneelem(l2) = ff then tt otherwise {if tl(l1) = e1l AND tl(l2) = e1l AND oneelem(l1) = tt then tt otherwise {if tl(l1) = e1l AND tl(l2) = e1l AND oneelem(l2) = ff then tt otherwise {if tl(l1) = e1l AND tl(l2) = e1e2l then tt otherwise {if tl(l1) = e2l AND tl(l2) = e2l AND oneelem(l1) = tt then tt otherwise {if tl(l1) = e2l AND tl(l2) = e2l AND oneelem(l2) = ff then tt otherwise {if tl(l1) = e2l AND tl(l2) = e2e1l then tt otherwise {if tl(l1) = e1e2l AND tl(l2) = e1e2l then tt otherwise {if tl(l1) = e2e1l AND tl(l2) = e2e1l then tt otherwise ff }}}}}}}}}}}; % In order to successfully guide INKA through the proof of the safety % lemma for prefix/aprefix, the following three auxiliary lemmata are % needed. % This first auxiliary lemma is proven automatically by INKA: all x,w,u,v:aelem all y,z:atail aprefix(quad(tt, ff, u, y), quad(tt, ff, v, z)) = tt -> aprefix(quad(tt, ff, w, combine(x, y)), quad(tt, ff, w, combine(x, z))) = tt; % Also the second auxiliary lemma is proven automatically by INKA: all u:aelem all v:atail aprefix(quad(tt, tt, u, combine(u, epsl)), quad(tt, ff, u, combine(u,v))) = tt; % To prove this third auxiliary lemma, interaction is necessary: all y,z:list all x:aelem prefix(y, z) = tt -> aprefix(quad(tt, ff, x, alphatail(y)), quad(tt, ff, x, alphatail(z))) = tt; % The safety lemma for prefix/aprefix. % (***NOT Automatically proven by INKA as of 20.4.00***) all l1,l2:list all n:nat prefix(l1,l2) = tt -> aprefix(alpha(l1),alpha(l2)) = tt;