tailieunhanh - Model-Based Design for Embedded Systems- P48

Model-Based Design for Embedded Systems- P48: This book contains information obtained from authentic and highly regarded sources. Reasonable efforts have been made to publish reliable data and information, but the author and publisher cannot assume responsibility for the validity of all materials or the consequences of their use. | 446 Model-Based Design for Embedded Systems These statements declare a unary function vertex and a binary function edge. The argument to vertex must be an integer while the arguments to edge must be vertex terms. These typed functions are undefined when applied to badly typed values otherwise they behave exactly like uninterpreted functions. This enrichment of the term algebra semantics with types leads naturally to an ordersorted-type system. We formalize this type system now. An order-sorted alphabet Lc is a structure Lç I A Li ieI The set I called the index set is a set of sort names alphabet names . Associated with each sort name i e I is a set of constants Li called the carrier of i. An order-sorted alphabet has the following properties L U Zi- i X j Li ç Lj ieI In other words L is the union of smaller alphabets and alphabets are ordered by set inclusion the sub-typing relation x is set inclusion. A type t is a term constructed from function symbols and elements of I or the special top-type T. Each type t identifies a subset t c TY L according to 1. The top type is the entire term algebra T Ty Z 2. A sort name t e I is just the carrier set LT Vt e I t Lt 3. Otherwise r f r1 T2 Tn where f is an n-ary function symbol IM v e Ty L V f V1 V2 . Vn A A vje N 1 j n The sub-typing relation x is extended to arbitrary types VTp rq rp A Tq Tp Ç Tq Expressive Constraints with Logic Programming Structural semantics often contain complex conformance rules these rules cannot be captured by simple-type systems. One common solution to this problem is to provide an additional constraint language for expressing syntactic rules such as the Object Constraint Language OCL 33 . Unlike other approaches we choose LP to represent syntactic constraints because Semantics of Domain-Specific Modeling Languages 447 1. LP extends our term algebra semantics while supporting declarative rules. 2. The fragment of LP supported by formula is equivalent to .