DOC PREVIEW
AUBURN COMP 7700 - PRINCIPLES IN FORMAL SPECIFICATION

This preview shows page 1-2-3-4-5 out of 15 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

IntroductionPatternsIntentA Terminological NoteA Methodological NoteSetting the SceneSemanticsStatic vs. Dynamic ModelsSyntaxReasoningThe Building Blocks of O-O ArchitectureParticipantsCollaborationsSpecification LanguagesDisCoConstraint DiagramsLePUSDesign Patterns’ FormalismsTool SupportGround RelationsRelations Among PatternsRefinementProjectionComparative CriteriaFuture DirectionsCompactnessConclusions and SummaryAcknowledgementsBiographiesReferencesPRINCIPLES IN FORMAL SPECIFICATION OF OBJECT ORIENTED DESIGN AND ARCHITECTURE Amnon H. Edeni Department of Computer ScienceConcordia University Montreal, Canada H3G 1M8 Yoram Hirshfeld Department of Mathematics Tel-Aviv University Tel Aviv 69978, Israel i Email: [email protected], phone: +1 (514) 848 3073, fax: +1 (514) 848 2830 Abstract Progress was made in the understanding of ob-ject-oriented (O-O) architectures through the in-troduction of patterns of design and architecture. Few works, however, offer methods of precise specification for O-O architectures. This article provides a well-defined ontology and an underlying framework for the formal specification of O-O architectures: We observe key regularities and elementary design motifs in O-O design and architectures; define “architec-tural model” in logic; and formulate relations be-tween specifications. We demonstrate how to de-clare and reason with the representations. Fi-nally, we use our conceptual toolkit to compare and evaluate proposed formalisms. Keywords: Software architecture, object oriented programming, formal foundations, software pat-terns 1. Introduction Architectural specifications provide software with “a unifying or coherent form or structure” [1]. Coherence is most effectively achieved through formal manifestations, allowing for unambiguous and verifiable representation of the architectural specifications. Various formalisms and Architecture Descrip-tion Languages (ADLs) [2] were proposed for this purpose, each of which derives from an estab-lished formal theory. For example, Allen and Gar-lan extend CSP [3] in Wright [4]; Dean and Cordy [5] use typed, directed multigraphs; and Abowd, Allen, and Garlan [6] chose Z [7] as the underly-ing theory. Other formalisms rely on Statecharts [8] and Petri Nets [9]. In contrast, techniques idiosyncratic to the ob-ject-oriented programming (OOP) paradigm, such as inheritance and dynamic binding [10], induce regularities of a unique nature. Consequently, O-O systems deviate considerably from other sys-tems in their architectures. We would expect the architectural specifications of O-O systems to re-flect their idiosyncrasies. Unfortunately, architectural formalisms have largely ignored the O-O idiosyncrasies. Few works (reviewed in Section 4) recognized the elementary building blocks of design and archi-tecture patterns. As a result of this oversight, any attempt to use formalisms for the specification of O-O architectures is destined to neglect key regu-larities in their organization. Only naturally, coherent specifications warrant the recognition of the underlying abstractions of the paradigm [11]. This is equally true for O-O programs. Therefore, we observe a small set of primitives (“building blocks”) that are proved suf-ficient to express O-O architecture. These include abstractions such as the inheritance class hierar-chies (Definition VI) and clans (Definition V), which are induced by the mechanisms of inheri-tance and dynamic binding, respectively. Havingobserved the underlying abstractions we can de-fine them formally and use them to defined the more elaborated constructions. Patterns More than any other form of documentation, soft-ware patterns [12, 13, 14, 15], in particular design patterns, were successful in capturing recurring motifs in O-O software architecture. Each pattern addresses a separate configuration of design or ar-chitecture, documented in a structured format, and distinguished by a name which carries its intent. Patterns carry abstractions that facilitate commu-nicating problems and solutions. Although the best insight into the regularities of O-O architecture is provided by the patterns lit-erature, it appears that the genre has not matured as a structured engineering domain. In particular, we observe two problems in this literature: 1. Ambiguity. The informal and ultimately fuzzy descriptions puzzle pattern users and cause substantial confusion. Even the very pattern writers demonstrate disagreement over their “true meaning” (e.g., [16, 17]). Debates that frequent patterns’ users in-clude the following: ♦ Instance-of (Definition III): Whether a particular implementation conforms to a certain pattern; ♦ Refinement (Definition VII): Whether one pattern is a special case of another. 2. Unstructured knowledge. With the growth in the number of patterns published, the accu-mulation of information is evolving into an unstructured mass which lacks any effective means of indexing. Clearly, these two problems result from the use of imprecise means of specification, such as ver-bal descriptions, class diagrams, and concrete ex-amples. This problem can be alleviated by provid-ing formal specifications, which may allow for unambiguous specifications, enable reasoning about the relationships between patterns (e.g., re-finement), and promote the structuring of the rap-idly growing body of patterns. 1.2 Intent This article introduces the following contribu-tions: 1. Define an ontology that serves as a frame of reference for the discussion in the essential concepts of O-O architecture. In particular: ♦ Observe the building blocks of O-O ar-chitecture, namely, a small set of elemen-tary ingredients that is sufficient to ex-press many architectures; ♦ Provide precise definitions for intuitive terms used with reference to O-O pat-terns; ♦ Establish relations between patterns which were of mere intuition or in dis-pute; 2. Analyse declarative formalisms for the speci-fication of O-O design patterns. In particular: ♦ Reconcile formalisms proposed by trans-lating sample expressions to our framework; ♦ Provide criteria for assessing the proper-ties of prospective specification lan-guages (e.g., expressiveness and com-pleteness). A Terminological Note Our use of the term pattern diverges from its use within the patterns community. Inspired by the work of Christopher Alexander [18, 19], a “pat-tern” is a prescription for solving a category of problems


View Full Document

AUBURN COMP 7700 - PRINCIPLES IN FORMAL SPECIFICATION

Download PRINCIPLES IN FORMAL SPECIFICATION
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view PRINCIPLES IN FORMAL SPECIFICATION and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view PRINCIPLES IN FORMAL SPECIFICATION 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?