--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on June 2012 ---
Hello Boris, 2012/6/26 Boris Hollas <hollas at informatik.htw-dresden.de>: > the constructor for predicate application Papp has a parameter of type > logic_info * (logic_label * logic_label) list * term list. > Was does the (logic_label * logic_label) list mean? If this has to do > with label binders (eg Pre, Here, Post), shouldn't this be a logic_label > list since a predicate can have an arbitrary positive number of labels, > eg foo_pred{L1,L2,l3}(x :int) = x >= 0 ? This is indeed use for label binders. More precisely, it is an association list from label parameters (as appearing in the declaration of the predicate) and the actual arguments. e.g., if you have predicate foo_pred{L1,L2,L3}(integer x); and apply it like foo_pred{Pre, Here, C_label}, the corresponding Papp constructor will be of the form Papp(_,[(L1, Pre); (L2,Old); (L3, C_label)],_) The fact that we use an association list and not a plain list of actual arguments is mainly historical. Best regards, -- E tutto per oggi, a la prossima volta Virgile