% auxiliary definitions of types used in feature models FEATURE_TYPES[ IDS: TYPE, % identificators for attributes AT: TYPE, % domain of attribute types AV: TYPE, % domain of attribute values FEATURE : TYPE % domain of features ] : THEORY BEGIN % a type of a feature is a record, that is a set of identifiers and mapping therof to their types FEATURE_TYPE : TYPE = [ ids : setof[IDS], typing: [(ids) -> AT] ] % typeof is a function that provides types for all features under consideration TYPEOF : TYPE = [ FEATURE -> FEATURE_TYPE ] END FEATURE_TYPES FEATURE_MODEL_GENERIC[ IDS: TYPE, AV: TYPE, AT: TYPE, TYPING: [AV -> AT], % typing for attribute values, each value has its type FEATURE : TYPE, (IMPORTING FEATURE_TYPES[IDS, AT, AV, FEATURE]) typeof: TYPEOF ] : THEORY BEGIN IMPORTING FEATURE_TYPES[IDS, AT, AV, FEATURE] % a domain assignment is a function that provides assignments for all features in the domain DOMAIN_ASSIGNMENT_GENERIC : TYPE = [ f : FEATURE -> [ (PROJ_1(typeof(f))) -> AV ] ] % a domain assignment provides proper assignments for all features w.r.t. given type system domain_assignment?(da: DOMAIN_ASSIGNMENT_GENERIC) : bool = forall(f: FEATURE): LET ft = typeof(f) IN % let ft be the type of the feature f FORALL (id: (PROJ_1(ft))): % for all the ids in the record TYPING(da(f)(id)) = PROJ_2(ft)(id) % the type of the assigned value has to be as the type prescribed by the type of f END FEATURE_MODEL_GENERIC FEATURE_MODELS[ IDS: TYPE, AV: TYPE, AT: TYPE, TYPING: [AV -> AT], FEATURE : TYPE, (IMPORTING FEATURE_TYPES[IDS, AT, AV, FEATURE]) typeof: TYPEOF ] : THEORY BEGIN IMPORTING FEATURE_MODEL_GENERIC[IDS, AV, AT, TYPING, FEATURE, typeof] % a type consisting of proper assignments of all features DOMAIN_ASSIGNMENT : TYPE = { da: DOMAIN_ASSIGNMENT_GENERIC | domain_assignment?(da) } % a type describing the selections functions SELECT: TYPE = [FEATURE -> bool] % a restriction function determines the admissible feature combinations % given a selection function and values for all the attributes % return true iff such a setup is a valid model RESTRICTION: TYPE = [ SELECT, DOMAIN_ASSIGNMENT -> bool ] % a specialization of a restriction function % is such a restriction function that does not allow any % new setups compared to the original model specialized?(refine: RESTRICTION, orig: RESTRICTION) : bool = FORALL (s: SELECT, da: DOMAIN_ASSIGNMENT): refine(s, da) IMPLIES orig(s, da) END FEATURE_MODELS % enumeration type for groups GROUP_TYPES : THEORY BEGIN GROUP_TYPE : TYPE = { FEATURE_GROUP, CLONE_GROUP } END GROUP_TYPES % introducing types describing feature groups FEATURE_GROUPS_TH[FEATURE: TYPE, GROUP: TYPE] : THEORY BEGIN FEATURE_GROUPS_GENERIC : TYPE = [ FEATURE -> setof[GROUP] ] feature_groups?(fg: FEATURE_GROUPS_GENERIC) : bool = % each group is used for partitioning of at most one feature's children FORALL (f1, f2: FEATURE): (NOT (f1 = f2)) IMPLIES (FORALL (g1: (fg(f1)), g2: (fg(f2))): NOT (g1 = g2)) % intersection(fg(f1), fg(f2)) = emptyset[GROUP]) FEATURE_GROUPS : TYPE = (feature_groups?) END FEATURE_GROUPS_TH % theory intorducing the type of a group-member function GROUP_MEMBERS_TH[FEATURE: TYPE, GROUP: TYPE, root: FEATURE] : THEORY BEGIN GROUP_MEMBERS_GENERIC : TYPE = [ GROUP -> setof[FEATURE] ] % this allows cycles on features that are not reachable from the root % but that does not cause any problems by the way the resctriction function is defined group_members?(gm: GROUP_MEMBERS_GENERIC) : bool = % no feature belongs into two groups % intersection(gm(g1), gm(g2)) = emptyset[FEATURE]) (FORALL (g1, g2: GROUP): NOT (g1 = g2) IMPLIES (FORALL (f1: (gm(g1)), f2: (gm(g2))): NOT (f1 = f2))) AND % root does not belong to a group (NOT (EXISTS (root_parent_group: GROUP): gm(root_parent_group)(root) )) GROUP_MEMBERS : TYPE = (group_members?) END GROUP_MEMBERS_TH % introducing the feature tree type FEATURE_TREES[ IDS: TYPE, AV: TYPE, AT: TYPE, TYPING: [AV -> AT], FEATURE : TYPE, GROUP: TYPE, % groups of features (IMPORTING FEATURE_TYPES[IDS, AT, AV, FEATURE]) typeof: TYPEOF, % typing of features (IMPORTING GROUP_TYPES) group_types: [ GROUP -> GROUP_TYPE ], root: FEATURE % the root of the structure ] : THEORY BEGIN IMPORTING FEATURE_MODELS[IDS, AV, AT, TYPING, FEATURE, typeof] IMPORTING FEATURE_GROUPS_TH[FEATURE, GROUP] IMPORTING GROUP_MEMBERS_TH[FEATURE, GROUP, root] FEATURE_TREE : TYPE = [# feature_groups : FEATURE_GROUPS, group_members : GROUP_MEMBERS, cardinalities : [ GROUP -> setof[nat] ] #] WALK_GENERIC : TYPE = [ l: posnat, [below(l) -> FEATURE] ] walk_from?(start: FEATURE, ft: FEATURE_TREE, w: WALK_GENERIC) : bool = LET seq = PROJ_2(w), n = PROJ_1(w) IN seq(0) = start AND % f is the last in the sequence (FORALL (i : below(n - 1)): % in each group there's a link-feature to to the next group, that is selected (EXISTS (g : (ft`feature_groups(seq(i)))): ft`group_members(g)(seq(i+1))) ) rooted_walk?(ft: FEATURE_TREE, w: WALK_GENERIC) : bool = walk_from?(root, ft, w) % form of the acycling lemma, in the form suitable for induction no_cycles : LEMMA FORALL (ft: FEATURE_TREE): FORALL (l: posnat): FORALL (w: { rw: WALK_GENERIC | rooted_walk?(ft, rw)} ): (l = PROJ_1(w)) IMPLIES (LET seq = PROJ_2(w), cp = seq(l - 1) IN (NOT (EXISTS (c: ({ fcp : WALK_GENERIC | walk_from?(cp, ft, fcp)})): PROJ_1(c) > 1 AND PROJ_2(c)(PROJ_1(c) - 1) = cp))) % proving that there can be a cycle on from any node that is reachable from the root acyclic : LEMMA FORALL (ft: FEATURE_TREE): FORALL (w: { rw: WALK_GENERIC | rooted_walk?(ft, rw)}): (LET l = PROJ_1(w), seq = PROJ_2(w), cp = seq(l - 1) IN (NOT (EXISTS (c: ({ fcp : WALK_GENERIC | walk_from?(cp, ft, fcp)})): PROJ_1(c) > 1 AND PROJ_2(c)(PROJ_1(c) - 1) = cp))) % given a selection function returns a subset of the selected features from a given set get_selected(select: SELECT, fs: setof[FEATURE]) : setof[FEATURE] = { f: (fs) | select(f) } % given a feature tree, a restriction defined by that tree is returned restriction(ft: FEATURE_TREE) : RESTRICTION = LAMBDA (select: SELECT, da: DOMAIN_ASSIGNMENT): select(root) AND (FORALL (f: FEATURE): % if a feature is selected there has to be a path of selected features to him from the root select(f) IMPLIES (EXISTS (n: posnat, seq: [below(n) -> FEATURE]): % there's a sequence of groups, s.t. seq(0) = root AND % root is the first in the sequence seq(n-1) = f AND % f is the last in the sequence (FORALL (i : below(n)): select(seq(i))) AND (FORALL (i : below(n - 1)): % in each group there's a link-feature to to the next group, that is selected (EXISTS (g : (ft`feature_groups(seq(i)))): ft`group_members(g)(seq(i+1))))) ) AND (FORALL (f: FEATURE): select(f) IMPLIES % if a feature is selected (FORALL (g: (ft`feature_groups(f))): % than for all his groups EXISTS (n: (ft`cardinalities(g))): % the cardinalities have to be satisifed % i.e., find a bijection from selected members of that group to below[n] EXISTS (b: [ ({ c : (ft`group_members(g)) | select(c) }) -> below[n] ] ) : bijective?(b)) % the cardinalities have to be selected ) % whenever a feature is a single member of a group with the cardinality [1..1], % then this feature is selected whener the owner of theat group is selected mandatory_lemma : LEMMA FORALL (ft: FEATURE_TREE, g: GROUP, mandatory_child: FEATURE) : (ft`cardinalities(g) = singleton(1) AND ft`group_members(g) = singleton(mandatory_child)) IMPLIES FORALL (select: SELECT, da: DOMAIN_ASSIGNMENT): restriction(ft)(select, da) AND % in any valid configuratoion (EXISTS (pf: FEATURE): select(pf) AND ft`feature_groups(pf)(g)) % if the parent is selected IMPLIES select(mandatory_child) % so is the mandatory child % whenever an owner of a group with the cardinality [1..1], is selected, % there has to be a single feauture from this group that is selected, alternative_lemma: LEMMA FORALL (ft: FEATURE_TREE, ag: GROUP): FORALL (select: SELECT, da: DOMAIN_ASSIGNMENT): restriction(ft)(select, da) AND ft`cardinalities(ag) = singleton(1) AND (EXISTS (pf: FEATURE): select(pf) AND ft`feature_groups(pf)(ag)) IMPLIES (EXISTS (unique : (ft`group_members(ag))): (FORALL (f : (ft`group_members(ag))): select(f) IFF f = unique) ) % whenever we a feature tree is obtained % from another feature tree by removing admissible cardinalities from a certain group, % the obtained feature tree is a specialization of the original one cardinality_spec : LEMMA FORALL (ft1, ft2: FEATURE_TREE, g: GROUP, gCard2: setof[nat]): LET gCard1 = ft1`cardinalities(g) IN (subset?(gCard2, gCard1) AND % ft2 = ft1 WITH [ `cardinalities := ft1`cardinalities WITH [ g := gCard2 ]]) ft2`feature_groups = ft1`feature_groups AND ft2`group_members = ft1`group_members AND ft2`cardinalities = ft1`cardinalities WITH [ g := gCard2 ]) IMPLIES specialized?(restriction(ft2), restriction(ft1)) % a function that given a feature tree, attribute, and a value, % returns a restriction function that requires the given value for the given attribute assign_value(ft: FEATURE_TREE, f: FEATURE, a : (PROJ_1(typeof(f))), val: ( {vv: AV | TYPING(vv) = PROJ_2(typeof(f))(a)} )) : RESTRICTION = LAMBDA (select: SELECT, da: DOMAIN_ASSIGNMENT): restriction(ft)(select, da) AND da(f)(a) = val % a function that given a feature tree, attribute, and a value, % returns a restriction function that requires the given value for the given attribute assign_value(restr: RESTRICTION, f: FEATURE, a : (PROJ_1(typeof(f))), val: ( {vv: AV | TYPING(vv) = PROJ_2(typeof(f))(a)} )) : RESTRICTION = LAMBDA (select: SELECT, da: DOMAIN_ASSIGNMENT): restr(select, da) AND da(f)(a) = val % assigning an attribute value is a specialization attr_spec1 : LEMMA FORALL (restr: RESTRICTION, f: FEATURE, a : (PROJ_1(typeof(f))), val: ( {vv: AV | TYPING(vv) = PROJ_2(typeof(f))(a)} )): specialized?(assign_value(restr, f, a, val), restr) % assigning an attribute value is a specialization attr_spec : LEMMA FORALL (ft: FEATURE_TREE, f: FEATURE, a : (PROJ_1(typeof(f))), val: ( {vv: AV | TYPING(vv) = PROJ_2(typeof(f))(a)} )): LET restr2 = assign_value(ft, f, a, val) IN specialized?(restr2, restriction(ft)) % requires specialization requires_spec(restr: RESTRICTION, requiree: FEATURE, required: FEATURE) : RESTRICTION = LAMBDA (select: SELECT, da: DOMAIN_ASSIGNMENT): restr(select, da) AND (select(requiree) IMPLIES select(required)) END FEATURE_TREES %%%%%%%%%% Examples of usage % a generic attribute value (a la union) AT_VALUE : DATATYPE BEGIN boolVal(bVal: bool): boolVal? intVal(iVal: int) : intVal? strVal(sVal: string) : strVal? END AT_VALUE % function prescribing types to AT_VALUE ATTRIBUTE_VALUE_TYPING : THEORY BEGIN IMPORTING AT_VALUE % type of attributes AT_TYPE : TYPE = { AT_BOOL, AT_INT, AT_STR } % assignment of types to values AT_TYPING : [ AT_VALUE -> AT_TYPE ] = LAMBDA (val: AT_VALUE): CASES val OF boolVal(boolVal): AT_BOOL, intVal(intVal): AT_INT, strVal(strVal): AT_STR ENDCASES END ATTRIBUTE_VALUE_TYPING % security profile example USING : THEORY BEGIN IMPORTING AT_VALUE IMPORTING ATTRIBUTE_VALUE_TYPING FEATURE_NAME : TYPE = { securityProfile, passwordPolicy, permissionSet } % the groups used in this feature model GROUP : TYPE = ({ fn: FEATURE_NAME | fn = passwordPolicy OR fn = permissionSet }) % a constant representing the set of features, % here, features are pairs of name and index % the convention is that clones use the index, where non-cloning featuers have a zero there, (e.g., clone_1, clon_2, f_0) % Q: -- could this be done in a nicer fashion? feature_set : setof[ [FEATURE_NAME, nat] ] = { f : [FEATURE_NAME, int] | f = (securityProfile, 0) OR f = (passwordPolicy, 0) OR (EXISTS (i:nat): f = (permissionSet, i)) } % feature type is composed of the features in the feature set FEATURE : TYPE = (feature_set) % securityProfile is the root root: FEATURE = (securityProfile, 0) % just one identificator, it could easily be just a set of all strings, this is more clear IDS: TYPE = { NAME } IMPORTING FEATURE_TYPES[IDS, AT_TYPE, AT_VALUE, FEATURE] % assigns types to our features typeof : TYPEOF = LAMBDA (f: FEATURE): CASES PROJ_1(f) OF securityProfile : ( emptyset[IDS], LAMBDA (id: (emptyset[IDS])) : AT_BOOL ), % no attributes passwordPolicy : ( emptyset[IDS], LAMBDA (id: (emptyset[IDS])) : AT_BOOL ), % no attributes permissionSet : ( singleton(NAME), LAMBDA (id: (singleton(NAME))) : AT_STR ) % a name attribute ENDCASES IMPORTING FEATURE_MODELS[IDS, AT_VALUE, AT_TYPE, AT_TYPING, FEATURE, typeof] IMPORTING GROUP_TYPES % assign types to our groups group_types : [ GROUP -> GROUP_TYPE ] = LAMBDA (g: GROUP): CASES g OF permissionSet : CLONE_GROUP, passwordPolicy : FEATURE_GROUP ENDCASES IMPORTING FEATURE_TREES[IDS, AT_VALUE, AT_TYPE, AT_TYPING, FEATURE, GROUP, typeof, group_types, root] % outfit groups with cardinalities cardinalities1 : [ GROUP -> set[nat]] = LAMBDA (g: GROUP): CASES g OF permissionSet : { n: nat | TRUE }, % permission set can be cloned ad libitum passwordPolicy : singleton(1) % passwordpolicy has to be included exactly once ENDCASES feature_groups1 : FEATURE_GROUPS = LAMBDA (f: FEATURE): CASES PROJ_1(f) OF securityProfile : { cg : GROUP | cg = permissionSet or cg = passwordPolicy }, passwordPolicy : emptyset[GROUP], permissionSet : emptyset[GROUP] ENDCASES group_members1 : GROUP_MEMBERS = LAMBDA (g: GROUP): CASES g OF permissionSet : { c: FEATURE | (EXISTS (i: nat): c = (permissionSet, i)) }, passwordPolicy : { c: FEATURE | c = (passwordPolicy, 0) } ENDCASES proj_groups : LEMMA FORALL (g: GROUP, f: FEATURE): group_members1(g)(f) IMPLIES PROJ_1(f) = g ft1 : FEATURE_TREE = (# feature_groups := feature_groups1, group_members := group_members1, cardinalities := cardinalities1 #) % this lemma proves that (passwordPolicy, 0) is in all configurations of ft1 passwordPolicyIs : LEMMA LET restriction = restriction(ft1) IN FORALL (da: DOMAIN_ASSIGNMENT, select: SELECT): restriction(select, da) IMPLIES select( (passwordPolicy, 0) ) % proving about a concrete configuration that it is a valid configuration, % i.e., showing that the model is consisten isAConfig : LEMMA LET select : SELECT = (LAMBDA (f: FEATURE): f = root OR f = (passwordPolicy, 0) OR f = (permissionSet, 0) OR f = (permissionSet, 1)), da: DOMAIN_ASSIGNMENT = LAMBDA (f: FEATURE): IF f = (permissionSet, 0) THEN LAMBDA (id: (singleton(NAME))): strVal("ace") ELSE IF f = (permissionSet, 1) THEN LAMBDA (id: (singleton(NAME))): strVal("loser") ELSE LAMBDA (id: (emptyset[IDS])): strVal("foo") ENDIF ENDIF IN restriction(ft1)(select, da) END USING % auxilliary theory for finite sequences of integers FIN_INT_SEQUENCES[len: nat] : THEORY BEGIN FIN_SEQUENCE : TYPE = [below(len) -> int] % sum first i elements of a given sequence sum_i(seq: FIN_SEQUENCE, i: upto(len)): RECURSIVE int = IF (i = 0) THEN 0 ELSE seq(i - 1) + sum_i(seq, i - 1) ENDIF MEASURE i % sum all the elements of the given sequence sum(seq: FIN_SEQUENCE) : int = sum_i(seq, len) END FIN_INT_SEQUENCES % satellite example SATELLITE_EXAMPLE : THEORY BEGIN IMPORTING AT_VALUE IMPORTING ATTRIBUTE_VALUE_TYPING FEATURE_NAME : TYPE = { satellite, storageControl, userDefinedApp, packetRouter, circuitSwitchedApp } IDS : TYPE = { APID, MaxStorageFieldSize, MaxUserMainMemory } % the groups used in this feature model GROUP_NAME : TYPE = { routerApp_gr, storageControl_gr, userDefinedApp_gr } GROUP : TYPE = { g: GROUP_NAME | g = routerApp_gr OR g = storageControl_gr OR g = userDefinedApp_gr } feature_set : setof[ [FEATURE_NAME, nat] ] = { f : [FEATURE_NAME, nat] | f = (satellite, 0) OR f = (storageControl, 0) OR f = (packetRouter, 0) OR f = (circuitSwitchedApp, 0) OR (EXISTS (i:nat): f = (userDefinedApp, i)) % clones for userDefinedApp } % feature type is composed of the features in the feature set FEATURE : TYPE = (feature_set) IMPORTING FEATURE_TYPES[IDS, AT_TYPE, AT_VALUE, FEATURE] udaIds : setof[IDS] = LAMBDA (id : IDS): id = APID OR id = MaxStorageFieldSize satIds : setof[IDS] = LAMBDA (id : IDS): id = MaxUserMainMemory % assigns types to our features typeof : TYPEOF = LAMBDA (f: FEATURE): CASES PROJ_1(f) OF userDefinedApp : ( udaIds, LAMBDA (id: (udaIds)): AT_INT ), % both attributes integers satellite : ( satIds, LAMBDA (id: (satIds)): AT_INT ) ELSE ( emptyset[IDS], LAMBDA (id: (emptyset[IDS])) : AT_BOOL ) ENDCASES IMPORTING GROUP_TYPES % assign types to our groups group_types : [ GROUP -> GROUP_TYPE ] = LAMBDA (g : GROUP): CASES g OF routerApp_gr: FEATURE_GROUP, storageControl_gr: CLONE_GROUP, userDefinedApp_gr: FEATURE_GROUP ENDCASES IMPORTING FEATURE_TREES[IDS, AT_VALUE, AT_TYPE, AT_TYPING, FEATURE, GROUP, typeof, group_types, (satellite, 0)] % outfit groups with cardinalities cardinalities1 : [ GROUP -> set[nat]] = LAMBDA (g: GROUP): CASES g OF routerApp_gr: LAMBDA (n: nat): n = 1, storageControl_gr: LAMBDA (n: nat): n = 0 OR n = 1, userDefinedApp_gr: LAMBDA (n: nat): TRUE ENDCASES feature_groups1 : FEATURE_GROUPS = LAMBDA (f: FEATURE): CASES PROJ_1(f) OF satellite : LAMBDA (g: GROUP): g = routerApp_gr OR g = storageControl_gr OR g = userDefinedApp_gr ELSE LAMBDA (g: GROUP): FALSE % emptyset otherwise ENDCASES group_members1 : GROUP_MEMBERS = LAMBDA (g: GROUP): CASES g OF routerApp_gr: LAMBDA (f: FEATURE): f = (packetRouter, 0) OR f = (circuitSwitchedApp, 0), storageControl_gr: LAMBDA (f: FEATURE): f = (storageControl, 0), userDefinedApp_gr: LAMBDA (f: FEATURE): PROJ_1(f) = userDefinedApp ENDCASES sat_ft : FEATURE_TREE = (# feature_groups := feature_groups1, group_members := group_members1, cardinalities := cardinalities1 #) IMPORTING FIN_INT_SEQUENCES % defining a restrtiction function for the satellite example, such that user defined app can't take more than % spec in the MaxUserMainMemory sat_restriction : RESTRICTION = LAMBDA (select: SELECT, da: DOMAIN_ASSIGNMENT): restriction(sat_ft)(select, da) AND (EXISTS (n: nat): (FORALL (f: FEATURE): (PROJ_1(f) = userDefinedApp AND PROJ_2(f) < n) IMPLIES select(f)) AND (FORALL (f: FEATURE): (PROJ_1(f) = userDefinedApp AND PROJ_2(f) >= n) IMPLIES NOT select(f)) AND LET attr_seq = LAMBDA (i: below(n)): iVal(da((userDefinedApp, i))(MaxStorageFieldSize)) IN sum[n](attr_seq) < iVal(da((satellite, 0))(MaxUserMainMemory)) ) % a valid example valid_conf : LEMMA LET select : SELECT = (LAMBDA (f: FEATURE): f = (satellite, 0) OR f = (packetRouter, 0) OR f = (userDefinedApp, 0) OR f = (userDefinedApp, 1)), da: DOMAIN_ASSIGNMENT = LAMBDA (f : FEATURE): IF PROJ_1(f) = userDefinedApp THEN LAMBDA (id : (udaIds)): CASES id OF APID : intVal(PROJ_2(f)), MaxStorageFieldSize : IF PROJ_2(f) = 0 THEN intVal(20) ELSE IF PROJ_2(f) = 1 THEN intVal(40) ELSE intVal(0) ENDIF ENDIF ENDCASES ELSE IF f = (satellite, 0) THEN LAMBDA (id : (satIds)): CASES id OF MaxUserMainMemory : intVal(100) ENDCASES ELSE LAMBDA (id : (emptyset[IDS])): strVal("foo") ENDIF ENDIF IN sat_restriction(select, da) % an invalid example, with exceeding memory invalid_conf : LEMMA LET select : SELECT = (LAMBDA (f: FEATURE): f = (satellite, 0) OR f = (packetRouter, 0) OR f = (userDefinedApp, 0) OR f = (userDefinedApp, 1)), da: DOMAIN_ASSIGNMENT = LAMBDA (f : FEATURE): IF PROJ_1(f) = userDefinedApp THEN LAMBDA (id : (udaIds)): CASES id OF APID : intVal(PROJ_2(f)), MaxStorageFieldSize : IF PROJ_2(f) = 0 THEN intVal(80) ELSE IF PROJ_2(f) = 1 THEN intVal(40) ELSE intVal(0) ENDIF ENDIF ENDCASES ELSE IF f = (satellite, 0) THEN LAMBDA (id : (satIds)): CASES id OF MaxUserMainMemory : intVal(100) ENDCASES ELSE LAMBDA (id : (emptyset[IDS])): strVal("foo") ENDIF ENDIF IN (NOT sat_restriction(select, da)) END SATELLITE_EXAMPLE