Verifying Abstractions in Model Checking ---------------------------------------- (Safety Lemma for Removing the head of a list) ------ Summary: Generalisation(?) 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. set_l ----- New type set_empty set_insert(alist, set_l) 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)) remhead ------- list -> list remhead(nil) = nil remhead(h::t) = t set_elem -------- (aelem, set_l) -> bool set_elem(E, set_empty) = false set_elem(E, set_insert(E, X)) = true (not (E = X)) -> set_elem(E, set_insert(X, T)) = set_elem(E, T) aremhead -------- alist -> set_l aremhead(quad(false, A, B, C)) = set_insert(quad(false, false, ne,eps1), set_empty) aremhead(quad(A, true, B, C)) = set_insert(quad(false, false, ne, eps1), set_empty) aremhead(quad(true, false, X, eps1)) = set_insert(quad(true, false, ne, eps1), set_insert(quad(true, true, ne, eps1), set_empty)) aremhead(quad(true, false, X, e1l)) = set_insert(quad(true, false, e1, eps1), set_insert(quad(true, true, e1, eps1), set_insert(quad(true, false, ne, e1l), set_empty))) aremhead(quad(true, false, X, e2l)) = set_insert(quad(true, false, e2, eps1), set_insert(quad(true, true, e2, eps1), set_insert(quad(true, false, ne, e2l), set_empty))) aremhead(quad(true, false, X, e1e21)) = set_insert(quad(true, false, ne, e1e2l), set_insert(quad(true, false, e1, e21), set_empty)) aremhead(quad(true, false, X, e1e11)) = set_insert(quad(true, false, ne, e1e1l), set_insert(quad(true, false, e2, e11), set_empty)) aremhead(quad(true, false, X, error)) = set_insert(quad(true, false, ne, error), set_insert(quad(true, false, e1, e1l), set_insert(quad(true, false, e1, e1e2l), set_insert(quad(true, false, e1, e2e1l), set_insert(quad(true, false, e1, error), set_insert(quad(true, false, e2, e2l), set_insert(quad(true, false, e2, e1e2l), set_insert(quad(true, false, e2, e2e1l), set_insert(quad(true, false, e2, error), set_empty))))))))) ------ Theorem: forall l: list set_elem(aplha(remhead(l)), aremhead(alpha(l))) ------ 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. ------ 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)); %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % removing the head of a list. function remhead(l:list):list = if l = nil then nil otherwise cdr(l); % The abstract remhead operation and the corresponding safety lemma. % We need a limited form of sets: We need to be able to insert new % elements and to test for membership. Using the predefined set type % of INKA is overkill, therefore we define our own limited set type, % implemented as lists. structure set_empty, set_insert(set_car:alist, set_cdr:set_l):set_l; predicate set_elem(e:alist, a:set_l) = if a = set_empty then false if a of set_insert and set_car(a) = e then true otherwise set_elem(e, set_cdr(a)); function aremhead(l:alist):set_l = if nonempty(l) = ff then set_insert(quad(ff, ff, ne, epsl), set_empty) otherwise {if oneelem(l) = tt then set_insert(quad(ff, ff, ne, epsl), set_empty) otherwise { if ord(l) = epsl then set_insert(quad(tt, ff, ne, epsl), set_insert(quad(tt, tt, ne, epsl), set_empty)) if ord(l) = e1l then set_insert(quad(tt, ff, e1, epsl), set_insert(quad(tt, tt, e1, epsl), set_insert(quad(tt, ff, ne, e1l), set_empty))) if ord(l) = e2l then set_insert(quad(tt, ff, e2, epsl), set_insert(quad(tt, tt, e2, epsl), set_insert(quad(tt, ff, ne, e2l), set_empty))) if ord(l) = e1e2l then set_insert(quad(tt, ff, ne, e1e2l), set_insert(quad(tt, ff, e1, e2l), set_empty)) if ord(l) = e2e1l then set_insert(quad(tt, ff, ne, e2e1l), set_insert(quad(tt, ff, e2, e1l), set_empty)) otherwise set_insert(quad(tt, ff, ne, error), set_insert(quad(tt, ff, e1, e1l), set_insert(quad(tt, ff, e1, e1e2l), set_insert(quad(tt, ff, e1, e2e1l), set_insert(quad(tt, ff, e1, error), set_insert(quad(tt, ff, e2, e2l), set_insert(quad(tt, ff, e2, e1e2l), set_insert(quad(tt, ff, e2, e2e1l), set_insert(quad(tt, ff, e2, error), set_empty)))))))))}}; % The safety lemma for remhead/aremhead. % ***NOT Automatically proven by INKA as of 20.4.00*** all l:list set_elem(alpha(remhead(l)), aremhead(alpha(l)));