Normalised( THEORY MagicNumberX IS MagicNumber(Implementation(TP3WinnieInterfaceImp))==(3.5) END & THEORY UpperLevelX IS First_Level(Implementation(TP3WinnieInterfaceImp))==(Machine(TP3WinnieInterface)); Level(Implementation(TP3WinnieInterfaceImp))==(1); Upper_Level(Implementation(TP3WinnieInterfaceImp))==(Machine(TP3WinnieInterface)) END & THEORY LoadedStructureX IS Implementation(TP3WinnieInterfaceImp) END & THEORY ListSeesX IS List_Sees(Implementation(TP3WinnieInterfaceImp))==(BASIC_IO) END & THEORY ListIncludesX IS List_Includes(Implementation(TP3WinnieInterfaceImp))==(TP3WinnieMachine); Inherited_List_Includes(Implementation(TP3WinnieInterfaceImp))==(TP3WinnieMachine) END & THEORY ListPromotesX IS List_Promotes(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListExtendsX IS List_Extends(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListVariablesX IS External_Context_List_Variables(Implementation(TP3WinnieInterfaceImp))==(?); Context_List_Variables(Implementation(TP3WinnieInterfaceImp))==(?); Abstract_List_Variables(Implementation(TP3WinnieInterfaceImp))==(?); Local_List_Variables(Implementation(TP3WinnieInterfaceImp))==(?); List_Variables(Implementation(TP3WinnieInterfaceImp))==(NbPlaces); External_List_Variables(Implementation(TP3WinnieInterfaceImp))==(NbPlaces) END & THEORY ListVisibleVariablesX IS Inherited_List_VisibleVariables(Implementation(TP3WinnieInterfaceImp))==(?); Abstract_List_VisibleVariables(Implementation(TP3WinnieInterfaceImp))==(?); External_List_VisibleVariables(Implementation(TP3WinnieInterfaceImp))==(?); Expanded_List_VisibleVariables(Implementation(TP3WinnieInterfaceImp))==(?); List_VisibleVariables(Implementation(TP3WinnieInterfaceImp))==(?); Internal_List_VisibleVariables(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListInvariantX IS Gluing_Seen_List_Invariant(Implementation(TP3WinnieInterfaceImp))==(btrue); Abstract_List_Invariant(Implementation(TP3WinnieInterfaceImp))==(btrue); Expanded_List_Invariant(Implementation(TP3WinnieInterfaceImp))==(NbPlaces: 0..600); Context_List_Invariant(Implementation(TP3WinnieInterfaceImp))==(btrue); List_Invariant(Implementation(TP3WinnieInterfaceImp))==(btrue) END & THEORY ListAssertionsX IS Abstract_List_Assertions(Implementation(TP3WinnieInterfaceImp))==(btrue); Expanded_List_Assertions(Implementation(TP3WinnieInterfaceImp))==(btrue); Context_List_Assertions(Implementation(TP3WinnieInterfaceImp))==(btrue); List_Assertions(Implementation(TP3WinnieInterfaceImp))==(btrue) END & THEORY ListInitialisationX IS Expanded_List_Initialisation(Implementation(TP3WinnieInterfaceImp))==(NbPlaces:=600); Context_List_Initialisation(Implementation(TP3WinnieInterfaceImp))==(skip); List_Initialisation(Implementation(TP3WinnieInterfaceImp))==(skip) END & THEORY ListParametersX IS List_Parameters(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListInstanciatedParametersX IS List_Instanciated_Parameters(Implementation(TP3WinnieInterfaceImp),Machine(TP3WinnieMachine))==(?); List_Instanciated_Parameters(Implementation(TP3WinnieInterfaceImp),Machine(BASIC_IO))==(?) END & THEORY ListConstraintsX IS List_Constraints(Implementation(TP3WinnieInterfaceImp),Machine(TP3WinnieMachine))==(btrue); List_Constraints(Implementation(TP3WinnieInterfaceImp))==(btrue); List_Context_Constraints(Implementation(TP3WinnieInterfaceImp))==(btrue) END & THEORY ListOperationsX IS Internal_List_Operations(Implementation(TP3WinnieInterfaceImp))==(XAjout_voiture,XRetire_Voiture,XNbLibre,XNbVoitures); List_Operations(Implementation(TP3WinnieInterfaceImp))==(XAjout_voiture,XRetire_Voiture,XNbLibre,XNbVoitures) END & THEORY ListInputX IS List_Input(Implementation(TP3WinnieInterfaceImp),XAjout_voiture)==(?); List_Input(Implementation(TP3WinnieInterfaceImp),XRetire_Voiture)==(?); List_Input(Implementation(TP3WinnieInterfaceImp),XNbLibre)==(?); List_Input(Implementation(TP3WinnieInterfaceImp),XNbVoitures)==(?) END & THEORY ListOutputX IS List_Output(Implementation(TP3WinnieInterfaceImp),XAjout_voiture)==(?); List_Output(Implementation(TP3WinnieInterfaceImp),XRetire_Voiture)==(?); List_Output(Implementation(TP3WinnieInterfaceImp),XNbLibre)==(?); List_Output(Implementation(TP3WinnieInterfaceImp),XNbVoitures)==(?) END & THEORY ListHeaderX IS List_Header(Implementation(TP3WinnieInterfaceImp),XAjout_voiture)==(XAjout_voiture); List_Header(Implementation(TP3WinnieInterfaceImp),XRetire_Voiture)==(XRetire_Voiture); List_Header(Implementation(TP3WinnieInterfaceImp),XNbLibre)==(XNbLibre); List_Header(Implementation(TP3WinnieInterfaceImp),XNbVoitures)==(XNbVoitures) END & THEORY ListPreconditionX IS Own_Precondition(Implementation(TP3WinnieInterfaceImp),XAjout_voiture)==(btrue); List_Precondition(Implementation(TP3WinnieInterfaceImp),XAjout_voiture)==(btrue); Own_Precondition(Implementation(TP3WinnieInterfaceImp),XRetire_Voiture)==(btrue); List_Precondition(Implementation(TP3WinnieInterfaceImp),XRetire_Voiture)==(btrue); Own_Precondition(Implementation(TP3WinnieInterfaceImp),XNbLibre)==(btrue); List_Precondition(Implementation(TP3WinnieInterfaceImp),XNbLibre)==(btrue); Own_Precondition(Implementation(TP3WinnieInterfaceImp),XNbVoitures)==(btrue); List_Precondition(Implementation(TP3WinnieInterfaceImp),XNbVoitures)==(btrue) END & THEORY ListSubstitutionX IS Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),XNbVoitures)==(btrue | @NbVoitures.((btrue | NbVoitures:=600-NbPlaces);(NbVoitures: NAT | skip))); Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),XNbLibre)==(btrue | @NbPlacesLibres.((btrue | NbPlacesLibres:=NbPlaces);(NbPlacesLibres: NAT | skip))); Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),XRetire_Voiture)==(btrue | @NbVoitures.((btrue | NbVoitures:=600-NbPlaces);(NbVoitures>0 ==> ((NbPlaces: 0..599 | NbPlaces:=NbPlaces+1);(" > Tartiflette retire": STRING | skip)) [] not(NbVoitures>0) ==> (" > Parking vide !": STRING | skip)))); Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),XAjout_voiture)==(btrue | @NbVoitures.((btrue | NbVoitures:=600-NbPlaces);(NbVoitures<600 ==> ((NbPlaces>0 | NbPlaces:=NbPlaces-1);(" > Voiture ajoute": STRING | skip)) [] not(NbVoitures<600) ==> (" > Parking de bananes !": STRING | skip)))); List_Substitution(Implementation(TP3WinnieInterfaceImp),XAjout_voiture)==(VAR NbVoitures IN NbVoitures <-- Get_NbVoitures;IF NbVoitures<600 THEN Ajout_Voiture;STRING_WRITE(" > Voiture ajoute") ELSE STRING_WRITE(" > Parking de bananes !") END END); List_Substitution(Implementation(TP3WinnieInterfaceImp),XRetire_Voiture)==(VAR NbVoitures IN NbVoitures <-- Get_NbVoitures;IF NbVoitures>0 THEN Retire_Voiture;STRING_WRITE(" > Tartiflette retire") ELSE STRING_WRITE(" > Parking vide !") END END); List_Substitution(Implementation(TP3WinnieInterfaceImp),XNbLibre)==(VAR NbPlacesLibres IN NbPlacesLibres <-- Get_NbLibre;INT_WRITE(NbPlacesLibres) END); List_Substitution(Implementation(TP3WinnieInterfaceImp),XNbVoitures)==(VAR NbVoitures IN NbVoitures <-- Get_NbVoitures;INT_WRITE(NbVoitures) END) END & THEORY ListConstantsX IS List_Valuable_Constants(Implementation(TP3WinnieInterfaceImp))==(?); Inherited_List_Constants(Implementation(TP3WinnieInterfaceImp))==(?); List_Constants(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListSetsX IS Context_List_Enumerated(Implementation(TP3WinnieInterfaceImp))==(?); Context_List_Defered(Implementation(TP3WinnieInterfaceImp))==(?); Context_List_Sets(Implementation(TP3WinnieInterfaceImp))==(?); List_Own_Enumerated(Implementation(TP3WinnieInterfaceImp))==(?); List_Valuable_Sets(Implementation(TP3WinnieInterfaceImp))==(?); Inherited_List_Enumerated(Implementation(TP3WinnieInterfaceImp))==(?); Inherited_List_Defered(Implementation(TP3WinnieInterfaceImp))==(?); Inherited_List_Sets(Implementation(TP3WinnieInterfaceImp))==(?); List_Enumerated(Implementation(TP3WinnieInterfaceImp))==(?); List_Defered(Implementation(TP3WinnieInterfaceImp))==(?); List_Sets(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListHiddenConstantsX IS Abstract_List_HiddenConstants(Implementation(TP3WinnieInterfaceImp))==(?); Expanded_List_HiddenConstants(Implementation(TP3WinnieInterfaceImp))==(?); List_HiddenConstants(Implementation(TP3WinnieInterfaceImp))==(?); External_List_HiddenConstants(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListPropertiesX IS Abstract_List_Properties(Implementation(TP3WinnieInterfaceImp))==(btrue); Context_List_Properties(Implementation(TP3WinnieInterfaceImp))==(btrue); Inherited_List_Properties(Implementation(TP3WinnieInterfaceImp))==(btrue); List_Properties(Implementation(TP3WinnieInterfaceImp))==(btrue) END & THEORY ListValuesX IS Values_Subs(Implementation(TP3WinnieInterfaceImp))==(aa: aa); List_Values(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListSeenInfoX IS Seen_Internal_List_Operations(Implementation(TP3WinnieInterfaceImp),Machine(BASIC_IO))==(INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE); Seen_Context_List_Enumerated(Implementation(TP3WinnieInterfaceImp))==(?); Seen_Context_List_Invariant(Implementation(TP3WinnieInterfaceImp))==(btrue); Seen_Context_List_Assertions(Implementation(TP3WinnieInterfaceImp))==(btrue); Seen_Context_List_Properties(Implementation(TP3WinnieInterfaceImp))==(btrue); Seen_List_Constraints(Implementation(TP3WinnieInterfaceImp))==(btrue); Seen_List_Precondition(Implementation(TP3WinnieInterfaceImp),STRING_WRITE)==(ss: STRING); Seen_Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),STRING_WRITE)==(skip); Seen_List_Precondition(Implementation(TP3WinnieInterfaceImp),CHAR_WRITE)==(cc: 0..255); Seen_Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),CHAR_WRITE)==(skip); Seen_List_Precondition(Implementation(TP3WinnieInterfaceImp),CHAR_READ)==(btrue); Seen_Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),CHAR_READ)==(@(cc$0).(cc$0: 0..255 ==> cc:=cc$0)); Seen_List_Precondition(Implementation(TP3WinnieInterfaceImp),BOOL_WRITE)==(bb: BOOL); Seen_Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),BOOL_WRITE)==(skip); Seen_List_Precondition(Implementation(TP3WinnieInterfaceImp),BOOL_READ)==(btrue); Seen_Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),BOOL_READ)==(@(bb$0).(bb$0: BOOL ==> bb:=bb$0)); Seen_List_Precondition(Implementation(TP3WinnieInterfaceImp),INT_WRITE)==(vv: NAT); Seen_Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),INT_WRITE)==(skip); Seen_List_Precondition(Implementation(TP3WinnieInterfaceImp),INTERVAL_READ)==(nn: NAT & mm: NAT & mm<=nn); Seen_Expanded_List_Substitution(Implementation(TP3WinnieInterfaceImp),INTERVAL_READ)==(@(bb$0).(bb$0: mm..nn ==> bb:=bb$0)); Seen_List_Operations(Implementation(TP3WinnieInterfaceImp),Machine(BASIC_IO))==(INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE); Seen_Expanded_List_Invariant(Implementation(TP3WinnieInterfaceImp),Machine(BASIC_IO))==(btrue) END & THEORY ListIncludedOperationsX IS List_Included_Operations(Implementation(TP3WinnieInterfaceImp),Machine(TP3WinnieMachine))==(Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures); List_Included_Operations(Implementation(TP3WinnieInterfaceImp),Machine(BASIC_IO))==(INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE) END & THEORY InheritedEnvX IS Operations(Implementation(TP3WinnieInterfaceImp))==(Type(XNbVoitures) == Cst(No_type,No_type);Type(XNbLibre) == Cst(No_type,No_type);Type(XRetire_Voiture) == Cst(No_type,No_type);Type(XAjout_voiture) == Cst(No_type,No_type)) END & THEORY ListVisibleStaticX END & THEORY ListOfIdsX IS List_Of_Ids(Implementation(TP3WinnieInterfaceImp)) == (? | ? | ? | NbPlaces | XAjout_voiture,XRetire_Voiture,XNbLibre,XNbVoitures | ? | seen(Machine(BASIC_IO)),imported(Machine(TP3WinnieMachine)) | ? | TP3WinnieInterfaceImp); List_Of_HiddenCst_Ids(Implementation(TP3WinnieInterfaceImp)) == (? | ?); List_Of_VisibleCst_Ids(Implementation(TP3WinnieInterfaceImp)) == (?); List_Of_VisibleVar_Ids(Implementation(TP3WinnieInterfaceImp)) == (? | ?); List_Of_Ids_SeenBNU(Implementation(TP3WinnieInterfaceImp)) == (?: ?); List_Of_Ids(Machine(TP3WinnieMachine)) == (? | ? | NbPlaces | ? | Ajout_Voiture,Retire_Voiture,Get_NbLibre,Get_NbVoitures | ? | ? | ? | TP3WinnieMachine); List_Of_HiddenCst_Ids(Machine(TP3WinnieMachine)) == (? | ?); List_Of_VisibleCst_Ids(Machine(TP3WinnieMachine)) == (?); List_Of_VisibleVar_Ids(Machine(TP3WinnieMachine)) == (? | ?); List_Of_Ids_SeenBNU(Machine(TP3WinnieMachine)) == (?: ?); List_Of_Ids(Machine(BASIC_IO)) == (? | ? | ? | ? | INTERVAL_READ,INT_WRITE,BOOL_READ,BOOL_WRITE,CHAR_READ,CHAR_WRITE,STRING_WRITE | ? | ? | ? | BASIC_IO); List_Of_HiddenCst_Ids(Machine(BASIC_IO)) == (? | ?); List_Of_VisibleCst_Ids(Machine(BASIC_IO)) == (?); List_Of_VisibleVar_Ids(Machine(BASIC_IO)) == (? | ?); List_Of_Ids_SeenBNU(Machine(BASIC_IO)) == (?: ?) END & THEORY VariablesLocEnvX IS Variables_Loc(Implementation(TP3WinnieInterfaceImp),XAjout_voiture, 1) == (Type(NbVoitures) == Lvl(btype(INTEGER,?,?))); Variables_Loc(Implementation(TP3WinnieInterfaceImp),XRetire_Voiture, 1) == (Type(NbVoitures) == Lvl(btype(INTEGER,?,?))); Variables_Loc(Implementation(TP3WinnieInterfaceImp),XNbLibre, 1) == (Type(NbPlacesLibres) == Lvl(btype(INTEGER,?,?))); Variables_Loc(Implementation(TP3WinnieInterfaceImp),XNbVoitures, 1) == (Type(NbVoitures) == Lvl(btype(INTEGER,?,?))) END & THEORY TCIntRdX IS predB0 == OK; extended_sees == KO; B0check_tab == KO; local_op == OK; abstract_constants_visible_in_values == KO END & THEORY ListLocalOperationsX IS List_Local_Operations(Implementation(TP3WinnieInterfaceImp))==(?) END & THEORY ListLocalInputX END & THEORY ListLocalOutputX END & THEORY ListLocalHeaderX END & THEORY ListLocalPreconditionX END & THEORY ListLocalSubstitutionX END & THEORY TypingPredicateX IS TypingPredicate(Implementation(TP3WinnieInterfaceImp))==(btrue) END & THEORY ImportedVariablesListX IS ImportedVariablesList(Implementation(TP3WinnieInterfaceImp),Machine(TP3WinnieMachine))==(NbPlaces); ImportedVisVariablesList(Implementation(TP3WinnieInterfaceImp),Machine(TP3WinnieMachine))==(?) END & THEORY ListLocalOpInvariantX END )