User Manual: Type System - Software and Systems Engineering
Contents
1. Figure 5 Starting Type Check Manually page 13 Type System of AutoFOCUS Figure 5 shows the start of the type check in AutoFOCUS2 The displayed menu appears if a component is selected and the right moue button is pressed In AutoFOCUS the type checker can be started within SSD using the key combination Strg T Within STDs the types are checked permanently and the results are displayed using configurable colors Figure 6 shows the results of an incorrect transition model in AutoFOCUS 5 isMoneyRequest i Tin i ToutINoMoney 5 isMoneyRequest i Tin o Tout withdrawMoney i m 5 not isMoneyRequest Tin i ToutlotherAction i Figure 6 Results of Type Checking in AutoFOCUS The types of the components in AutoFOCUS can be defined at the ports and the channels of the components If the defined type is more general than the inferred type the inferred type is displayed in square brackets For example of if we define a channel with a generic type in AutoFOCUS using the type variable a type variables are prefixed using a which is connected to a Port with a concrete type Int than the type Int is inferred for the channel and the connected ports and displayed in square brackets out a Int A A 41 O see Figure 7 Figure 7 Inferred Types in SSDs Note that the inferred types within the components e g from the Automaton are not propagated into the SSDs in AutoFOCUS Hence the page 14 Type2. main maindeclsemi maindeclsemi maindecl maindecl datadecl typedecl impldecl importdecl instancedecl fundecl arrterm qid id qualid coid id number decimal hexnumber sign Est snumber sign number temporal lt gt IO po EE tempneg temporal neg sampleinit init terml importdecl import qid import qid instancedecl instance type in id where funinstance andfun andfun and funinstance funinstance fun infixline altinfix infixline pat binop pat tterm altinfix infixline binop z Type System of AutoFOCUS lt 18 gt te Sa te pe mem 8 e datadecl stereo data id datargs dconstr altdconstrs derivingclass datargs id coid altdconstrs dconstr dconstr stereo id stereo id selector type coseltype coseltype selector type selector id derivingclass deriving id coid typedecl stereo type id range snumber to snumber deltanumber stereo type id fixed snumber to snumber deltanumber sizenumber stereo type id datargs type deltanumber delta number sizenumber size number impldecl stereo implementation id implterm addimplterm implterm 1 id idecl coidecl coidecl ide
3. DTDModules Every DTDModule corresponds to one textual document in AutoFOCUS called DTD The module concept of AutoFOCUS allows to use qualified names of the form lt DTDModuleName gt lt element gt and to import elements from other DTDModules such they can be used without qualification in the DTDModule Since AutoFOCUS components cannot declare import statements for referencing elements from DTDModules they have to use qualified names if the referenced elements are not unique in the symbol table For example if two constants max exist in two DTDModules M1 and M2 the components have to refer them as Ml max and M2 max while the DTDModule M3 can refer max without qualification as max if it has been imported by declaring import Ml max or import M2 within the DTDModule page 8 Type System of AutoFOCUS 1 5 Implementation Types The concept of implementation types allows to refine numeric types The goal of using implementation types is to validate the models numeric properties as it will be computed on target hardware with restricted numeric features For example many processors do not support floating point arithmetic but only integer arithmetic Therefore the floating point values of the model have to be replaced by fixed point approximations on the target Implementation types allow to model and simulate these approximations within AutoFOCUS and support therefore the detection of numeric errors within the model For this purpose
4. LowerBound String Precision String Arity int infix boolean DataDef UpperBound String LowerBound String Precision String Bits int Prio int lt lt ordered gt gt Discriminator 0 Assertion MIF Term Constructor Selector lt lt ordered gt gt ae 5 1 Figure 9 Meta Model of AutoFOCUS Type System Terms The meta model for terms is depicted in Figure 10 page 30 Type System of AutoFOCUS ar ered gt gt p Comte Name String Text String Hr mn Comment lt lt ofdered gt NEM Name String een MIF Term Head Arity int Inft lt boolean Prio int fesertion MIF Term er E lt lt ordered gt gt Q Figure 10 Meta Model of Terms The elements in the model are Term is the abstract class for all terms in AutoFOCUS see Section 1 1 Var is the class for variables Variables are unique in terms e g the x S in x 2 x refer to the identical object Variables have the following attributes o Name String the name of the variable Appl is the class for applications An application has a head Const and at least one argument Applications have the following attributes o Assertion MIFTerm the assertion of the application Note that only applications in the definitions of functions can have assertions that restrict t
5. e g data PosInt assert num x gt 0 gt gt PN num Int e ConstDef represents the definition of user defied constants and functions ConstDefs have the following attributes o Name String the name of the defined constant o Text String the complete definition of the constants Comments and formatting information is ignored in this attribute For an identical text only the Text attribute of DTDModules can be used since this is set before parsing the module o Comment Comment a textual attachment for the definitions This is used to textually store the stereotypes of the definition page 32 Type System of AutoFOCUS e Constructors are specific constants Constructors are defined by data definitions Constructors can be applied in pattern matching definitions Every constructor with arguments has selector functions Selector to select the arguments of the data definition The number of selector functions is equal to the arity of the constructors e Selector see Section 4 2 2 Every selector belongs to it s constructor One constructor can have several selectors e Discriminator see Section 4 2 2 Every discriminator belong to exactly one constructor 5 2 Types The meta model of types and implementation types is depicted in Figure 11 TypeDef TConst lt lt key gt gt Name String sskey gt gt Name String THead RangeType Abstract Type Implementation Type UpperBou
6. Import The grammar for the AutoFOCUS module system see Section 1 4 is importdecl import qid import qid page 29 Type System of AutoFOCUS 5 Models The AutoFOCUS parser generates models from the textual syntax The models are as all other modeling concepts of AutoFOCUS specified using a so called meta model The meta model of AutoFOCUS provides the API to develop new applications It is described in AFMM This section repeats the meta model of the type system and explains it more detailed The overall model is depicted in Figure 9 The most important parts are described in the following subsections D Typelmpl Implementation DTD key Abstract Type lt skey gt gt Name String Implemented Type B FlmportedModules Comment a RN ti E DTD Module G D efined Type ordered zs T A ConstDef F nu y Name String TypeClass z 1 Text String lt lt key gt gt Name String JA VA Comment Comment eS Args g lt lt o dered gt Ds de D x 0 7 mE Ine t ea o7 TypeClassinstantiation Var Appl e lt key gt gt Name String A lt skey gt gt Name String Assertion MIF Term lt ckey gt Name String E i Hed rom THead Les RangeType f Sy AbstractType Implementation Type UpperBound String
7. In the first line the inferred type for the variable x is a type variable a and the type of test is restricted to Bool a gt a In the second pattern the type of the different variable x is inferred to another type variable b the type of the function test is restricted to b NUM gt NUM combining it with the first type of test the resulting type for test is Bool NUM gt NUM This is the defined type of the function test If the type of test should be more specific a more concrete signature definition can be added e g test Bool Int gt Int In this case the defined type of test is set to the specified type Bool Int gt Int 3 2 Atomic Rules The types of constants and functions are inferred from their definitions A constant can be defined as a constant or function than the defined type is inferred as described in the previous section If a constant or page 17 Type System of AutoFOCUS function is a constructor of a data type the type is directly used from the type definition Default constants are constants that have no user defined definition are assigned to types as follows e True Bool False Bool e Numeric values without comma are numeric values NUM e Numeric values with comma are Float values 3 3 Propagation The propagation of types in terms ensures that the most general type of the terms is inferred The most general types are stored in application terms which are separate objects and variables
8. have the following attributes o UpperBound Term upper bound of the range o LowerBound Term lower bound of the range o Precision Term precision step width of the range type e ImplementationType is an implemented fixed point term see Section 4 2 4 Implementation types have the following attributes o UpperBound Term upper bound of the range o LowerBound Term lower bound of the range o Precision Term precision step width of the range type o Bits int the number of required bits 5 3 Type Classes The meta model of type classes and instantiations is depicted in Figure 12 page 35 Type System of AutoFOCUS TypeClass sskey Name String lt lt key gt gt Name String Arity int Inft lt boolean Prio int Fesertion MIF Term QE TypeClassinstantiation ConstDef lt lt key gt gt Name String TA Dae qn sube Comment Comment Figure 12 Meta Model of Type Classes Every type can belong to a type class EQ ORD NUM The most specific class is noted If there a no classes available for a type the relation is empty As described in Section 1 3 and Section 4 2 2 the type class instantiations TypeClassInstantiation instantiate a type constructor TConst into a type class Additional requirements on the type classes of the arguments of the type constructor are modeled by the association from TypeClassInstantiation to TypeClass Every TypeClassInstantiation can prov
9. DTD contains references to DTDModules which can contain imported DTDModules Some Elements like type definitions are not used in DTDs therefore they are only contained in their defining modules The meta model for modules is depicted in Figure 13 EU aa zi Importedhtodules TN Toe TN lt lt key gt gt Name String Text String D D PA sskey gt gt Name String A pay n Ho Infix boolean Prio int Assertion MIF Term sskey gt gt Name String ConstDef TypeDef Name String Text String Figure 13 Meta Model of Modules The used elements of in the meta model of Modules are e DTD The DTD is the container for all elements With the indexed associations to type constants modules type classes and constants and functions the DTD is the symbol table of the component and page 37 Type System of AutoFOCUS can be used for determining if the types and terms of the component are correct e DTDModule is a module of the language A DTD module corresponds to a file of a programming language or a DTD element of AutoFOCUS DTDModules can import other DTDModules DTDModules contain all constructs of the module They have the following attributes o Name String the name of the module o Text Stringthe textual representation of the module page 38 Type System of AutoFOCUS 6 Predefined Elements The predefined elements of AutoFOCUS can be used in al
10. System of AutoFOCUS defined types of the ports of the component are used for checking the complete system This modularity feature of the type checker in AutoFOCUS allows to type check large models without checking all subcomponents Therefore the types of the components should not be more general than the used types within the components In AutoFOCUS2 the type checking is deep i e includes all subcomponents and their descriptions If the types are not propagated as expected a complete type check of the project is recommended page 15 Type System of AutoFOCUS 3 Type Inference Type inference assigns concrete types to the untyped variables and applications in a term e g type inference of x 1 assigns the type NUM from the constant 1 to the variable x and the type Bool to the term consisting of the application of to x and 1 Similar inferences are applied to infer the types and type classes of type variables The type context stores the inferred types of the variables and type variables The results of the type inference are stored in the model mostly in the Type Field such that they can be displayed and used in all model based applications of type checked models The results are only stored in variables and applications since the constants are global and can be used in different contexts their inferred types must not be stored at the constants The inferred types of constants are stored in the type contexts and are set in th
11. Type System of AutoFOCUS User Manual Type System Abstract The type system of AutoFOCUS describes the data modelling language with the possibilities of defining and inferring types in AutoFOCUS models This description includes the concepts grammars and inference rules and relevant subsets Furthermore open issues implementation bugs are described The type system of AutoFOCUS has been developed by Validas AG within the BMBF project AutoMODE in cooperation with TU Munich and ETAS GmbH VAVAV VALIDAS validated quality page 1 Type System of AutoFOCUS Contents A o A eee eee 4 2 Basic Concepts and DefinitiOns rrrrrrrrnnnnnnnvvnnnnvnnnnnnnnnnnvnnnnnnnnnnnnnnnnnvnnnnnnnnnnnnnn 5 2 1 O 5 A erect 5 sired cases cance eo veg EE E A noes tac A E cegec et 6 2 3 O tat esttachac eels i Sate ae tug cde ena E RTE 7 DA Module CONCEP li iS 8 2 5 Implementation Typs eie rie tese enean ii 9 CAMERE CISMRTII MRB A LIT E M 13 A TYPO DINGO rFence cui E t 16 4 1 Context of Type Infe renes orient maa 16 427 Ames ss 17 4 3 A 18 Br SYMA eres 19 5 1 A A A e 19 5 1 1 BEE EE one E enna E O aE S R n NN Ea ot 19 5 1 2 Variables di 19 5 1 3 APPEARS 20 5 1 4 SEIS EEE RET ENE TE 21 E s p rci dee NR KM sere cecil cts lace etna cette N 22 5 1 6 User Dem SR 23 IL Teve 25 5 2 1 Type LeS eraga sedans a ee 25 5 2 2 Data DeDnittonsz oto t IP ai 25 5 2 3 T
12. ailable in all subcomponents SSD Editor lt edit gt Defaultimplementation ST 58 Tools Options Help A Cut Strg xX Copy Strg C Associations Attributes Property Strg P Sub Structure Refine Strg R Local Variables Data Strg D Parameter Definitions Strg G Implementation Parameters Strg l Font Strg F ausilnt int10 o Select all Strg A Check all Types Strg T Delete Strg Entf Figure 4 Implementation Parameters Since it might be much work to specify an implementation for every type separately AutoFOCUS supports two helpful concepts 1 If only one implementation is applicable to the type this mapping is used 2 If there exists an implementation called Default this implementation is selected page 11 Type System of AutoFOCUS The computation of the implemented type for a port or local variable is done as follows 1 select the implementation mapping as follows a the user has explicitly selected an implementation or b there exists a Default Implementation 2 The available implementations are searched bottom up from the current component until the top component 3 compute the implemented type from the mapping by finding the Typelmpl pair of types for which the abstract type matches the type of the port The concrete type of the Typelmpl is the implemented type of the port variable Within the API of AutoFOCUS there are three different functions to access t
13. ame of the partial selector functions can be specified by the user rest in the example If not specified the default name consists of the Name of the Constructor Sel and the number of the position of the selector e g ConsSel1 for the first selector of Cons Every user defined function that uses pattern matching can be translated into a function that uses discriminators and selectors This is important for generating code into low level languages like C or Java The equivalent function to a user defined function can be computed using the API call Term tFunCase af TermUtils getFunctionTerm ConstDef The grammar for data declarations is datadecl stereo data id datargs dconstr altdconstrs derivingclass datargs id coid altdconstrs dconstr dconstr stereo id stereo id selector type coseltype coseltype selector type selector id derivingclass deriving id coid To determine the type class of the type terms like List Int or List Bool the instantiations of the type constructor into type classes are important An instantiation consists of a type information and a definition of the characteristic functions of that class For example one page 26 Type System of AutoFOCUS could defined the operation on lists such that all non empty lists are equal However in general there exists a canonical definition of that identifies lists only if they c
14. are the identifiers that can be used in the type terms An example for a type term is Bool Store Int If Store is a user defined type TConst this type is used otherwise a type variable is generated in the type term Type terms can be defined using the following rules type id id id type cotype type id type cotype cotype type arrtype gt type Note that currying is not supported There are no higher order functions in AutoFOCUS Therefore the functional type arrtype can only be used once in signature declarations see Section 4 1 6 but not in arbitrary terms 4 2 2 Data Definitions Data definitions are the basis of functional programming languages They define the identifiers that can be used in type terms and the constructors for the pattern matching in the functions In addition to the features of many functional languages AutoFOCUS data declarations also define so called selector and discriminator functions for the type page 25 Type System of AutoFOCUS For example the definition of infinite lists is data List a Nil Cons a rest List a deriving ORD defines not only the constructors Nil and Cons and the type constructor List but also the following discriminator and selector functions fun is Nil Nil True is Nil False fun is Cons Cons x1 x2 True is Cons False fun ConsSell Cons x1 x2 xl fun rest Cons x1 x2 x2 The n
15. cl idecl type gt type addimplterm implterm fundecl stereo funline altline page 46 Type System of AutoFOCUS stereo constdef id type id type cotype arrtype funline fun line constdef const id tterm altline line line stereo pat tterm tpat pat typean pat id number char string id tpat copat copat tpat tterm interm typean interm arrterm in arrterm arrterm arrterm arrterm tterm termO term0 terml termO terml SAU termO terml SEU termO terml terml term2 gt terml term2 lt gt terml term2 when terml term2 sample term2 sampleinit term2 default terml term2 term2 term3 term2 term3 fby term2 term3 term3 term4 amp amp term3 term4 term4 term5 bor term4 term5 page 47 Type System of AutoFOCUS term5 term6 bxor term5 terme term6 term7 band term6 term7 term term8 term8 term8 z term8 term8 term8 terms term8 term9 lt term9 term9 lt term9 term9 gt term9 term9 gt term9 term9 term9 term10 term9 term10 gt gt term9 term10 gt gt gt term9 term10 term10 termll terml0 termll terml0 termll termll terml2 termll term12 termll term12 termll term12 terml2 si
16. d Double however code generators generate different code Float Double from them 6 4 Casts For all numeric types there exist casting functions in AutoFOCUS with the expected types e Abstract Types O O O Float2Int Int2Float Double2Int Int2Double Double2Float Float2Double page 41 Type System of AutoFOCUS e Range Type Int4 O O O O O int4uint4 int4uint8 int4uint16 int4uint32 int4uint64 int4int8 int4int16 int4int32 int4int64 e the same for int8 to uint64 6 5 Classes The predefined type classes are mentioned in Section 1 3 page 42 Type System of AutoFOCUS 7 Open Issues No import for components hence all elements are imported and overloading is resolved arbitrarily if no qualification is used Sets and manual type class instantiations are currently not completely implemented as described Type abbreviations are currently not checked correctly page 43 Type System of AutoFOCUS 8 References AF The tool AutoFOCUS available at http autofocus in tum de AF2 The tool AutoFOCUS2 available at http www4 in tum de af2 Haskell The programming language Haskell available at http www haskell or AFMM Description of the AutoFOCUS meta model and it s API Included in the distribution of AutoFOCUS in lt AFHOME gt usermanuals ValidasAPI pdf page 44 Type System of AutoFOCUS A AutoFOCUS Grammar The complete Grammar see Help of DTD Editor is
17. e applications using the constants 3 1 Context of Type Inference The type inference depends on the context A component with a specific type can be type correct in one context but may not fit into another context If the type check is started in a component only this component is checked but not it s context If a project is type checked all top components in the projects are checked Another important feature for the type inference is the binding mechanism of type variables Type variables are identified only within one component description hence a shared component with a type using the variable a can have different types in different instantiations in different components Within one component type variables with the same name e g a are identified Note that type variables NUM EQ and ORD are not identified such that components with type classes can be used in different instantiations within the same component see example in Figure 8 page 16 Type System of AutoFOCUS i1 NUM Int e 012 NUM Int o i2 NUM Int e Int i3 NUM Float hd 034 NUM Float 3 i4 NUM Float e l Figure 8 Mixing Types in AutoFOCUS The context of the type checking in DTDs Data Type Definitions is only relevant for checking user defined functions Every function patterns has it s own context and the resulting type for the function is combined over all patterns For example a function fun test True x x test 3 0 15
18. e type classes of the type fit together Type variables are used in the definition of types e g by defining the type of lists of arbitrary elements To avoid misspelling errors in types for example by typing imt8 instead of ints type variables must start with a i e if a port shall have the general type which can be matched with any other type the type name for this port must be a Note that AutoFOCUS has the functional type constructor gt for describing the types of functions For simplicity values must not have functional types The arity of gt is two however it can have also more arguments for example the type of is NUM NUM NUM page 6 Type System of AutoFOCUS 1 3 Type Classes Type classes are used for defining functions that operate on different types For example the function that checks if an elements is in a list of arbitrary elements should not have the type list a gt Bool but the type list EQ gt Bool EQ requires that the instantiated types provides an equality operation for comparing elements A type class is a set of types For simplicity AutoFOCUS supports only the following three type classes e EQ e ORD is a specialization of EQ i e all types in ORD belong also to EQ e NUM is a specialization of ORD If a type has no class it does not belong to any of these classes This is the most general case Every type class is characterized by the presence of some characteristic operations
19. els that are used to represent terms in AutoFOCUS A user defined constant and a user defined function has a definition from the user All other constants and functions are called default page 5 Type System of AutoFOCUS constants and default functions Examples for default constants and functions are True 1 and 1 2 Types Every term in AutoFOCUS has a type A type describes a set of possible values The user can define a type for a term and the types can be inferred For example the type of True is Bool which describes the possible values True and False and the type of 1 is NUM which describes all numeric values The user can define the type of a term by writing type annotations for example 1 Int or by defining signatures for functions e g max NUM gt NUM In this case there is not only a type but also a defined type Note that defined types can also be more general than the inferred types especially in component models where types are specialized by propagating between connected components Types can be constructed like terms from type constants type variables and type building functions type constructors Examples for type constants are Bool and Int An example type constructor is set which is denoted by curly brackets It can be used to construct the types like Int or Bool The number of arguments a of a type constructor is also called it S arity A type variable can be instantiated by type terms if th
20. er an element is in a set is expressed using the infix operation in e g 3 in 1 2 3 Furthermore subsets with predicates can be formulated using e g x x gt 1 x lt 10 On the left side of the pattern matching can be applied to define variables for the right side E G x Bool x True or IPair x y x y Note that with this notation also infinite sets could be specified e g the pair example if IPair is defined as a general data constructor data IntPair IPair Int Int A set is finite if it consists only of finite enumerated boolean or constructed from user defined constructors over finite types data types Note that the operators any and rnd can be inefficient if restrictions are used since they base on a simple generate and check approach For example the value any BPair x y y x is using the Boolean Pairs data BoolPair IBPair Int Int computed as follows BPair False False is generated and checked for False False The next generated value is BPair True False which satisfies True False and is therefore the result of the any operation rnd uses random values instead of page21 Type System of AutoFOCUS incremental generation Functions over finite sets e g the sum of the values in the set can be build using the any operator and the difference fun sumOfValues s if s then 0 else let x any s in x sumOfValues s x fi To make the specifications of set functions more
21. erm12 termll term12 termll term12 The grammar for the prefix notation requires an identifier followed by brackets with the function arguments separated by comma terml2 id term coterm coterm term In addition to the infix and prefix terms some special mixfix application terms can be build if then else let terms sets and arrays Furthermore there are some special terms like case or merge in the grammar however they are used for special purposes and therefore cannot be used in all situations The set and array terms are described in the following sections The rules for special terms are term12 if tterm then tterm else tterm fi page 20 Type System of AutoFOCUS let id arrterm in terml2 The let term is a special term which allows to assign variables in a sequential way For example in the function definition fun f x let y x x in let z y y in z y 1 4 1 4 Sets AutoFOCUS allows to build finite sets of elements All elements in the set have to be of the same type In contrast to weakly typed languages the elements in the set must be of the same monomorphic type Sets like 1 True are forbidden Sets can be constructed using set brackets and The curly brackets are also used to denote the type of sets E g the type Int is the type of set of integers Furthermore it is possible to add subtract sets using and is used for intersection of sets The test wheth
22. for an implementation is the following definition implementation myImpl Float gt int32 TT gt uint8 Note that implementations can be extended by existing implementations using the operators such that Fine Int gt int32 myImpl is also a valid implementation For every port and local variable in the implemented model one mapping has to be selected If there is more than one mapping for the type of the port variable defined a selection box appears that allows to choose the desired implementation see Figure 2 The resulting implemented type is displayed using gt type in the selection box Implementation gt Result Fine gt int10 v Fine gt int10 Figure 2 Selecting an Implementation for an AutoFOCUS Port If implementation types are used the type checker infers the implemented types In the model the implemented type is displayed as gt type see Figure 3 page 10 Type System of AutoFOCUS ein NUM Int int10 aus Int gt int10 C Figure 3 Display of Implemented Types in SSDs SSDs have to be reusable in different context Sharing with different implementations This requires that once a type of Port ein is implemented using Fine and in another context using Precise SSDs have implementation parameters An implementation parameter is declared in the SSD like a parameter or a local variable see Figure 4 Like parameters the implementation parameters are av
23. gn tempneg idorsize tterm coterm if tterm then tterm else tterm fi let id arrterm in term12 sign tempneg tterm ET tterm coterm D t tterm coterm t E sign tempneg qid a char V4 tterm tterm coterm Wy string page 48 Type System of AutoFOCUS sign neg number case tterm then tterm else tterm esac merge tterm then tterm else tterm egrem coterm tterm idorsize id size typean type type id id id type cotype type id type cotype cotype type arrtype gt type important lexical helpers LMIMLMPMMIIMMMMMMEIMMPMMMMMEMEIMMPII decimal digit digit Stereo not gt not gt not gt not gt string not quote char not char n NO NET AX Vort hexnumber Ox OX digit A F I a uus MEUS Y neg not qualid letter letter alpha id dollar letter alpha page 49
24. h 1 Stored 2 True matches the second definition of search with the values x 1 and y 2 The result of evaluating the term is False 12 2 The rules for user definitions are fundecl stereo funline altline stereo constdef id type id type cotype arrtype constdef const id tterm altline line line stereo pat tterm tpat pat typean pat id number char string id tpat copat copat tpat As can be seen from the grammar also signatures can be declared e g for defining the type of the constant If signatures are missing the most general type for the constant function is inferred In the above example of max the inferred type is NUM if this is too general the type can be restricted to Int by max Int const max 100 50 page 24 Type System of AutoFOCUS 4 2 Types Types can be assigned to every term see Section 4 1 Furthermore model elements like ports have types Similar to terms there can be different types variables TVar constants TConst and complex applications TAppl Like terms have types types have type classes see Section 1 3 The available type constants are the default types and the user defied types data definitions type abbreviations range and implementation types 4 2 1 Type Terms The type terms consist of the special types for sets arrays and functions The names of the default and user defined types
25. he different types e getDefinedTypeModel returns the user defined type e getType returns the inferred type from the type checker e getimplementedType returns the type from the implementation If there is no implementation available the original type is returned Note that these functions can only return defined values if the type checking has been applied page 12 Type System of AutoFOCUS 2 Using Type System The type system of AutoFOCUS is an advanced consistency check of the models The terms used within the models have to be type correct The operation to ensure that the model elements are type correct is called type check Not that the semantics of AutoFOCUS is only defined for type correct models i e incorrect models cannot be treated Therefore the type check is executed before all operations that base on the semantics of AutoFOCUS like simulation code generation and model checking In addition to this build in checks the type checker can be started manually for the complete project or for some parts of the model components automata transitions DTDs E 12 MCTest Or H 8 Ports LocVariables eS Channels n Edit characteristic map E New DTD e Create Mode J Create State HBT Model Checking Generate Java Code Simulation EH Associate Motivate Paste Component Cut Component Copy Component Open Editor Ki Rename Node X Delete Node
26. he possible parameter of a function but do not affect the pattern matching during the evaluation Assertions of functions can be specified using stereotype For example by fun lt lt assert x 0 gt gt f x 1 x In this case the term associated with the definition ConstDef of f is an Appl and has the assertion associated page 31 Type System of AutoFOCUS e Const describe constants and functions User defined constants have exactly one definition ConstDef For example const c 0 5 Examples for constants are c 1 True and neg Using type instantiations see Section 4 2 2 and 5 3 the predefined constants like can have several ConstDefs with Type Class instantiations Constants have the following attributes o Name String the name of the constant functions o Arity int the number of arguments the constant function requires o Infix boolean is true for infix operations like o Prio int the priority of the operation Priorities are used for printing the terms without redundant brackets e g a b c instead of a b c o Assertion MIFTerm is the assertion that is fulfilled of the function or the constant Assertions to Const can be specified using stereotypes of the form lt lt assert term E g assert f x gt 0 gt gt fun f x x 1 If the Const is a Constructor function the assertion restricts the possible arguments Constructor assertions are specified in the data definition of the constructors
27. he software to an embedded target without floating point unit In order to ease the definition and use of implementation types there are two possibilities integrated in AutoFOCUS It suffices to fix the size or the delta of implementation types Some examples for the definition of implementation types are type impl8 fixed 10 0 to 10 0 size 8 inferred delta type impl8 fixed 10 0 to 10 0 delta 0 1 inferred size page 28 Type System of AutoFOCUS The grammar for the implementation types is typedecl stereo type id fixed snumber to snumber deltanumber sizenumber deltanumber delta number sizenumber size number sign t snumber sign number 4 2 5 Range Types Range types describe subsets of existing types They consist of upper and lower bounds For numeric types also a delta can be provided Some examples for the definition of range types are type rt range 1 to 11 delta 2 type pos range 1 to 100 type SomeColors range Red to Blue The grammar for the range types is typedecl stereo type id range snumber to snumber deltanumber 4 2 0 Casts Casts are ordinary functions in AutoFOCUS that have to be provided if variables of different types are used For example x int8 y int8 int16 is not type correct but int8int16 x int8 y int8 int16 is correct For all pairs of numeric types there are casts available see Section 6 4 4 3 Modularity
28. ide several definitions ConstDefs for the overloaded constants called characteristic constants Since the predefined constants can have different instantiations every constant can have several ConstDefs However user defined constants have exactly one ConstDef without TypeClassInstantiation The definition of the meta model of type classes uses the following elements e Type classes are modeled in TypeClass Every type class knows it s characteristic operations association to Const A SuperClass relation between type classes as in Haskell is not needed for AutoFOCUS since no user defined type classes are supported o Name String the name of the type class e TypeClassInstantiation describes the instantiation of a type into a class page 36 Type System of AutoFOCUS 5 4 Modules The modules in the type system build the basis of type checking Every AutoFOCUS component can have it s own DTD with different DTDModules The DTD is the symbol table for parsing terms All elements in the DTD are unique such that it suffices to compare the objects instead of the references The symbol table DTD is used for parsing and type checking for example it contains constants and types during parsing these objects are used it the elements are not found in the DTD variables are generated Usually the data types are defined globally since some mechanisms like importing rely on a global unique naming convention of DTDModules The
29. in AutoFOCUS The main design goals for the languages was to have a well defined simple but also expressive and functional language as sound basis for modelling embedded systems This document describes the expression languages of AutoFOCUS including the main feature of type inference and checking It is intended to serve as an introduction for advanced AutoFOCUS modellers AutoFOCUS models can also be build without user defined types and functions of this language and also for developers which want to write their own model based analyses or generators for specific targets Note that many features like indexed arrays range types type class instantiations sets have not been tested intensively such that there might occur bugs This manual is structured as follows Section 1 introduces the basic concepts informally Section 2 shows how to use the type system Section 3 informally describes the inference rules In Section 4 the syntax of AutoFOCUS is explained Advanced concepts not explained in the introduction are also described Section 4 Section 5 describes the meta models of the type system Section 6 lists the predefined elements The manual closes with open issues and references Section 7 and Section 8 page 4 Type System of AutoFOCUS 1 Basic Concepts and Definitions AutoFOCUS is strongly typed i e every term in the model has a fixed type The type must not be totally fixed monomorph but can be polymorphic For exam
30. ixline pat binop pat tterm page 27 Type System of AutoFOCUS altinfix infixline lt Ve z gt 4 The only instances that are allowed are those that instantiate into the binop sema VEN l ri var v r 1g 1 known classes EQ ORD NUM The instances must not be complete for example the operation in EQ can be derived from however the arithmetic operations have to be provided completely 4 2 3 Type Abbreviations Type abbreviations introduce new names for complex types For example if the type NUM is used frequently it can be referred using a symbolic name This name can be defined by a type abbreviation For example type NA NUM The type checker does not differentiate between NA and NUM However the type of 1 2 can only be inferred as NUM and is not simplified to NA If 1 2 NA is desired it has to be specified The grammar for type abbreviations is typedecl type id datargs type 4 2 4 Implementation Types Implementation types are discrete types that are used to implement floating point types on embedded computers that have no floating point units Implementation types have a fixed size e g 8 bits and a range e g from 10 0 to 10 0 For fixed size and the range a distance between the values can be computed using the formula delta 2 bits 1 range Implementation types are integrated into AutoFOCUS to simulate the effect of deploying t
31. l specification The realization definition is in the class af SymbolTable which contains the static definitions of the elements 6 1 Constants The following constants are predefined in AutoFOCUS e Constructor True Bool e Constructor False Bool e Constructor NoVal Channel a Note that all constants using the channel type are internal and should not be used in the AutoFOCUS models For specific applications like property formulation for model checking these constants can be helpful 6 2 Functions The following functions are predefined in AutoFOCUS e Const not Bool gt Bool e Const size a gt NUM e Const let in e Constif then else fi Bool a a gt a e Const al e Const s e Const s e Constructor NoVal m gt Channel m e Discriminator is Msg Channel m gt Bool e Discriminator is NoVal Channel m gt Bool e Selector Val Channel m gt m e Const length String gt NUM e Const prio 1 gt Bool Bool gt Bool for implication e Const prio 2 gt Bool Bool gt Bool for biimplication page 39 Type System of AutoFOCUS Const prio 2 Const prio 3 amp amp Const prio 4 bor Const prio 5 bxor Const prio 6 band Const prio 7 Const prio 7 Const prio 7 Bool Bool gt Bool for disjunction Bool Bool gt Bool for conjunction NUM NUM gt NUM for bitwise or NUM NUM gt NUM for bitwise exc
32. lusive or NUM NUM gt NUM for bitwise and a a gt Bool for equality EQ EQ gt Bool for inequality EQ EQ gt Bool for weak equality Const prio 8 NUM NUM gt Bool Const prio 8 lt NUM NUM gt Bool Const prio 8 gt NUM NUM gt Bool Const prio 8 gt Const prio 8 in Const prio 9 Const prio 9 Const prio 9 Const prio 10 Const prio 10 NUM NUM gt Bool s s Bool for containment in sets NUM NUM gt NUM for left shift NUM NUM gt NUM for right shift NUM NUM gt NUM for unsigned right shift NUM NUM gt NUM NUM NUM gt NUM Const NUM gt NUM for unary minus Const NUM gt NUM for unary plus Const prio 11 Const prio 11 Const prio 11 NUM NUM gt NUM NUM NUM gt NUM NUM NUM gt NUM Some internal constants are available in the symbol table for temporal logic and clock operations 6 3 Types The following predefined types exist in AutoFOCUS Abstract Types o Bool o Int o Float page 40 Type System of AutoFOCUS O O Double Char String for building sets for building arrays gt for building functional types Range types O O O O O bit with values O and 1 int4 int8 int16 int32 int64 uint4 uint8 uint16 uint32 uint64 Note that since AutoFOCUS uses exact representations of values there is no difference between Float an
33. nd String bo Que int UpperBound String LowerBound String Infi boo le an Lower Bound String Precision String NE PENE Figure 11 Meta Model of Types e Type is an abstract class for types e TypeDef is a definition of a user defined type Type definitions can have type variables if functional types like list a are defined They page 33 Type System of AutoFOCUS have the following attributes o Name String the name of the defined type o Text String the textual representation of the definition without formatting and comments For an identical text only the Text attribute of DTDModules can be used since this is set before parsing the module e AbbrevDef is a special form of type definitions TypeDef see Section 4 2 3 The new defined type is a type constant TConst possibly with variables The expanded type is the associated type of the AbbrevDef e DataDef is a special form of type definitions TypeDef see Section 4 2 2 The data definition has associations to the defined constructors e TVar represents a type variable By default all types that are not specified will be type variables TVars are unique in terms e g the a S x a y a refer to the same object Every type identifier that is not defined predefined or user defined will be treated as a type variable To avoid errors in modeling components due to misspelling of identifiers e g imt8 will be a type variable since int8 is predefined but im
34. ontain the same elements in the same order Of course this is only possible if the elements in the list support belong to the class EQ AutoFOCUS tries to derive such operations and instantiations automatically if the declaration has a deriving attachment If subclasses are specified as ORD in the above example the super classes are also derived The default derived order is the order that bases on the order in which the data constructors are specified e g Nil lt Cons x 1 If the constructors are identical the arguments are compared using their order Arithmetic operations are derived by point wise extension of the constructor arguments E g the addition on pairs is defined by adding both components in the pair However this works only for types with exactly one constructor In the above list example no numeric operations can be derived In this case the instantiations have to be specified manually In the list example this could look as follows fun listAdd Nil X X listAdd X Nil X listAdd Cons x1 r1 Cons x2 r2 Cons x1 x2 listAdd r1 r2 instance List NUM in NUM where fun x y listAdd x y and fun x y listSub x y ann fun x y listMult x y and fun x y listMod x y and fun x y listDiv x y The grammar for type instantiations is instancedecl instance type in id where funinstance andfun andfun and funinstance funinstance fun infixline altinfix inf
35. ple the polymorphic type NUM stands for arbitrary numeric values and can be instantiated by monomorphic types like Int Float Or uint8 1 1 Terms Values are the informations that are exchanged by AutoFOCUS Values can be default values like 1 True 1 2 or they can be constructed using constructors from other values e g the and for constructing sets Constructors for a user defined type can be defined in user defined type definitions Constructors can also have no arguments in this case they construct the values without arguments like constant functions without arguments Constructors can be used in pattern matching see Section 4 1 6 Terms are the descriptions of values Examples of terms are 1 True 2 3 three and f x Every value is a term but also user defined constants variables and functions can be used in terms A variable can be instantiated by concrete values if type of the variable and the type of the value fit together AutoFOCUS uses variables for modelling input of the components e g the x in the input pattern ein x is a variable and within function definitions A function is applied to it s arguments values and computes a new value The number of arguments of a function is called it s arity Examples for functions are with arity 2 and with arity 1 in the case of f x The user can define constants like three 1 2 and functions like f x x 1 see Section 4 1 6 Section 5 1 describes the mod
36. quotes hello world and sign can be or Negation can be formulated using or neg Numbers can be defined as decimal or hexadecimal numbers according to the following rules number decimal hexnumber decimal digit digit hexnumber Ox OX digit A F a f 4 1 2 Variables Variable terms are build by their names E g x The scope of the variables depends on their context This can either be a function definition which uses variables or can be a transition page 19 Type System of AutoFOCUS The grammar for variables is the same as for constants e g variables are constants with names that have be bound in a context terml2 sign neg qid 4 1 3 Applications Application terms consist of a function called header and their arguments The header function is modeled as a constant The arity of the header has to be equal to the number of arguments of the application Applications can be build with the build in infix operations e g 1 x or with prefix notation e g f x y Infix operations use the usual binding priorities to reduce the number of required brackets in terms like 2 lt 1 2 3 The build in functions and their priorities are described in Section 6 2 The infix rules form a large part of the AutoFOCUS grammar all follow the same scheme The following rules show some examples termlO0 termll terml0 termll terml0 termll termll terml2 termll t
37. readable they can be formulated using pattern matching with a special pattern For example fun sumOfValues 0 sumOfValues x s x sumOfValues s The rules in the grammar for defining sets are apart from the application of functions which is described in Section 4 1 3 term12 Ups wg tterm coterm tterm tterm coterm j tterm interm typean interm arrterm in arrterm arrterm The rules for tterm and arrterm denote that the infix operator in has the lowest priority since all other infix operators are defined in the rules for the non terminal arrterm 4 1 5 Arrays Arrays are structures of fixed size of similar values that can be accessed using indices In AutoFOCUS the default array index is the type Int starting with the index 0 however other index types can be used Arrays can be declared In this case the type is constructued by square brackets 1 E g an arrays of Boolean values is declared as follows ba Bool If the index type shall also be declared this can be done using a comma E g the above declaration is equivalent to ba Bool Int The access to page 22 Type System of AutoFOCUS the values is per index e g ba 0 or ba 1 Arrays can be constructed using the square brackets e g 4 5 6 Furthermore arrays can be defined with index values e g 1 5 0 4 2 6 This case can be useful if other index types are desired Note that the indice
38. s must be a sequence i e no value must be missing like in 1 5 4 4 2 6 The size of an array i e the umber of elements in it can be computed using the size function The rules for defining and accessing arrays are arrterm arrterm tterm terml2 tterm coterm There is no iteration construct for arrays The sum of values over an array has to be computed recursively over the size of the array E g using the following definition fun arrSum a arrIndSum a 0 fun arrIndSum a i if size a i then 0 else a i arrIndSum a i 1 fi 4 1 6 User Definitions The user can define constants and functions in AutoFOCUS Constants are global static definitions that assign values to named constants For example const max 100 50 Functions can be defined using pattern matching A pattern is either a variable or a constructor of the appropriate type applied to the number of patterns the constructor requires An example for a function with pattern matching is defined over an user defined type data Store Empty Stored Int Bool fun search x Empty False search x Stored y True x y page 23 Type System of AutoFOCUS search x Stored y False x y The semantics of the functions is that the first maching pattern is executed i e the variables in the pattern are bpund to concrete values and the right hand side of the function definition is executed For example the term searc
39. t8 is not known type variables in SSDs should start with a quote e g a In DTDs this is not required TVars have the following attribute o Name String the name of the type variable e TAppl type applications are type terms i e applications of functional types to type arguments For example the type list a is an application of the functional type list to the type argument a The relation THead represents the constant head of the term list in the example the ordered association TArgs represents the arguments of the type application term a in the example e TConst are the abstract class of atomic parts of types in page 34 Type System of AutoFOCUS AutoFOCUS Type constants can be abstract types and implementation types Type constants have the following attributes o Name String the name of the type constant e AbstractType represents the unimplemented types of AutoFOCUS Abstract types can be type constants or functional types Type constants can be default type constants like Float Bool or functional types like or gt or user defined types data and range types Abstract types have the following attributes o Arity int the number of argument the abstract type requires o Infix boolean is true for the infix type gt e RangeType is an abstract type with the description of a range see Section 4 2 5 A range is defined by a TypeDef It restricts an abstract type with a lower and an upper bound RangeTypes
40. that can be used for defining operations on that type The characteristic operations for the type classes in AutoFOCUS are e EQ o equal EQ EQ gt Bool o inequal EQ EQ gt Bool e ORD o less ORD ORD gt Bool o less or equal lt EQ EQ gt Bool o greater gt EQ EQ gt Bool o greater or equal gt EQ EQ gt Bool e NUM o addition NUM NUM gt NUM o subtraction NUM NUM gt NUM o multiplication NUM NUM gt NUM o division NUM NUM gt NUM If a type belongs to a type class it provides the characteristic operations of that class For example the type Boo1 only belongs to the type class EQ page 7 Type System of AutoFOCUS e g terms like True X are correctly types while True gt x or True False are not correct User defined types can be instantiated into a specific type class in two ways 1 by automatically deriving the characteristic functions from the order of the constructors and the characteristic operations of the used types 2 by manually defining the characteristic functions This features is currently not supported in AutoFOCUS but the models and the syntax are present such that it can be integrated if this features is needed 1 4 Module Concept The user defined definitions of types and functions can be modular The Symbol Table represented by the DTD in AFMM of AutoFOCUS components consists of all defined functions and constants in the
41. there are two different simulations in AutoFOCUS integrated the ordinary simulation which used the defined types and the implementation simulation which uses the implemented types see Figure 1 for starting the implementation simulation IES Windows Help Consistency Check Types Strg T Simulation Restart Simulations Remove Simulations Remove all Simulations Figure 1 Starting Implementation Simulation in AutoFOCUS Mapping AutoFOCUS integers with unrestricted size to integers of fixed size is a similar challenge Another benefit of implementation types is that general models can be restricted to small ranges This allows to verify the model using model checking Note that currently the model checking extension does not explore this feature Using implementation types consist of two parts 1 Definition of fixed point types This can be omitted if the predefined integer types see Section 6 3 are used 2 Mapping the general types to fixed point types page 9 Type System of AutoFOCUS It suffices to specify the mapping for the ports and local variables in the system The other used elements terms constants and functions are inferred from the type system The mapping has to be defined using so called implementations An implementation consists of type implementations called Typelmpl in AFMM that map abstract types to concrete types Implementations are defined in the data type definition An example
42. which are unique within one term The propagation of types identifies the types of variables in all occurrences of the term and the arguments of functions with the expected types Furthermore type annotations are integrated into the propagation For example type checking the term x y Int gt 0 infers the type x Int from the type annotation y Int from the application of NUM NUM gt NUM to the y Int and 0 Int from the result of gt ORD ORD gt Bool applied to the Int result of the addition page 18 Type System of AutoFOCUS 4 Syntax The actual syntax of the AutoFOCUS can be seen in the help grammar menu of the DTD Editor In the following the most important rules and the related concepts if not explained in Section 1 are explained 4 1 Terms There can be three different terms in AutoFOCUS models constants variables and applications like in the lambda calculus These are described in the following subsections Sets and arrays are special form of terms and are described separately 4 1 1 Constants Constants are referred by their names or directly by the values The following rules of the AutoFOCUS grammar describe the definition of constants in AutoFOCUS terms terml2 sign neg qid char string sign neg number Where qid are possibly qualified identifiers see Section 1 4 char refers to characters ec string refers to arbitrary text without escape characters included in
43. ype AbbreviatloNnS ato iria 28 5 2 4 Implementation Types cese erret et eee ae Pe eee YE YR ERES a Reed g e EN 28 529 RET pvr 29 5 2 6 ER EE EE E TE EN 29 5 3 Mod larity Mpo ae E 29 Type System of AutoFOCUS 6 Models iii corrida 30 6 1 MO el eee alate a has Lan cad 30 Ged TIPS in td se 33 6 3 Te Use 35 6 4 Modules ii b esL 37 7 Predefined Elements nnnunnnnnnnnnnnnnnnnunnnnnnnnunnnnnnnunnnnnnnnunnnnnnnunnnnnnnnnnnnnnnnunnnnnnnunnene 39 7 1 ConStants ust tddi dia 39 72 os A let edit bd cee trwturs aduptelthe aat 39 7 3 O o P 40 7 4 SA eee none 41 7 5 AA ean eden 42 8 Open AAA HY 43 97 References dicos 44 A AUTOFOCUS Grammar annnnnnnannnnunnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnunnnnnnnnnnnnnnnnnnnnnnnnn 45 page 3 Type System of AutoFOCUS Introduction This documentation describes the type system of AutoFOCUS AF It has been developed from Validas AG within the BMBF Project AutoMODE and is currently integrated into the tool AutoFOCUS2 AF2 from TU Munich While AutoFOCUS supports different type systems for different purposes by allowing to create different projects with different languages Currently the supported languages are Java Quest AutoMODE In AutoFOCUS2 there is only one language realized In this document we describe the type system of AutoFOCUS which is the type system of AutoFOCUS2 and identical to the type system of the AutoMODE language projects
Download Pdf Manuals
Related Search