• Definitions of software engineering (SE)
  • Historical origins of SE
  • SE as part of systems engineering
  • SE consists of many activities in addition to programming
  • SE and other disciplines


  • The application of engineering to software
  • Field of computer science dealing with software systems
    • large and complex
    • built by teams
    • exist in many versions
    • last many years
    • undergo changes

Definitions (cont')

  • Application of a systematic, disciplined, quantifiable approach to the development, operation, and maintenance of software (IEEE 1990)
  • Multi-person construction of multi-version software (Parnas 1978)

Role of SE in system design

  • SE part of larger projects
  • Embedded
    • Software requirements to be balanced against others
      • e.g., telephone switching systems
        • certain requirements  can only be met by hw, sw, and special devices


  • The field of software engineering was born in 1968 in response to chronic failures of large software projects to meet schedule and budget constraints 
    • Recognition of "the software crisis"
  • Term became popular after NATO Conference in Garmisch Partenkirchen (Germany), 1968

Role of software engineer

  • Programming skill not enough
  • Software engineering involves "programming-in-the –large"
    • understand requirements and write specifications
      • derive models and reason about them
    • master software 
    • operate at various abstraction levels
    • member of a team
      • communication skills
      • management skills

The software lifecycle (a preview)

Relationships between SE and other CS disciplines

  • Programming languages
  • Operating systems
  • Data bases
  • Artificial intelligence
  • Theory

Relationships between SE and other disciplines

  • Management science
  • Systems engineering
  • Others


    • Software engineering (SE) is an intellectual activity and thus human-intensive
    • Software is built to meet a certain functional goal and satisfy certain qualities
    • Software processes also must meet certain qualities
    • Software qualities are sometimes referred to as “ilities”

    Software product

    • Different from traditional types of products
      • intangible
        • difficult to describe and evaluate
      • malleable
      • human intensive
        • involves only trivial “manufacturing” process

    Classification of sw qualities"ilities"

    • Internal vs. external
      • External -> visible to users
      • Internal -> concern developers
    • Product vs. process
      • Our goal is to develop software products
      • The process is how we do it
    • Internal qualities affect external qualities
    • Process quality affects product quality


    • Software is correct if it satisfies the functional requirements specifications
      • assuming that specification exists!
    • If specifications are formal, since programs are formal objects, correctness can be defined formally
      • It can be proven as a theorem or disproved by counter examples (testing)

    The limits of correctness

    • It is an absolute (yes/no) quality
      • there is no concept of “degree of correctness”
      • there is no concept of severity of deviation
    • What if specifications are wrong?
      • (e.g., they derive from incorrect requirements or errors in domain knowledge)


    • Reliability
      • informally, user can rely on it
      • can be defined mathematically as “probability of absence of failures for a certain time period”
      • if specs are correct, all correct software is reliable, but not vice-versa (in practice, however, specs can be incorrect …)

    Idealized situation

    • Requirements are correct


    • Robustness
      • software behaves “reasonably” even in unforeseen circumstances (e.g., incorrect input, hardware failure)


    • Efficient use of resources
      • memory, processing time, communication
    • Can be verified
      • complexity analysis
      • performance evaluation (on a model, via simulation)
    • Performance can affect scalability
      • a solution that works on a small local network may not work on a large intranet


    • Expected users find the system easy to use
    • Other term: user-friendliness
    • Rather subjective, difficult to evaluate
    • Affected mostly by user interface
      • e.g., visual vs. textual


    • How easy it is to verify properties
      • mostly an internal quality
      • can be external as well (e.g., security critical application)


    • Maintainability: ease of maintenance
    • Maintenance: changes after release 
    • Maintenance costs exceed 60% of total cost of software
    • Three main categories of maintenance
      • corrective: removing residual errors (20%)
      • adaptive: adjusting to environment changes (20%)
      • perfective: quality improvements (>50%)
    • Can be decomposed as
      • Repairability
        • ability to correct defects in reasonable time
      • Evolvability
        • ability to adapt sw to environment changes and to improve it in reasonable time


    • Existing product (or components) used (with minor modifications) to build another product
      • (Similar to evolvability)
    • Also applies to process
    • Reuse of standard parts measure of maturity of the field


    • Software can run on different hw platforms or sw environments
    • Remains relevant as new platforms and environments are introduced (e.g. digital assistants)
    • Relevant when downloading software in a heterogeneous network environment


    • Ease of understanding software
    • Program modification requires program understanding


    • Ability of a system to coexist and cooperate with other systems 
      • e.g., word processor and spreadsheet

    Typical process qualities

    • Productivity
      • denotes its efficiency and performance
    • Timeliness
      • ability to deliver a product on time
    • Visibility
      • all of its steps and current status are documented clearly

    Timeliness: issues

    • Often the development process does not follow the evolution of user requirements
    • A mismatch occurs between user requirements and status of the product

    Timeliness: a visual description of the mismatch

    Application-specific qualities

    • E.g., information systems
      • Data integrity
      • Security
      • Data availability
      • Transaction performance.

    Quality measurement

    • Many qualities are subjective
    • No standard metrics defined for most qualities


    • Principles form the basis of methods, techniques, methodologies and tools
    • Seven important principles that may be used in all phases of software development
    • Modularity is the cornerstone principle supporting software design
    • Case studies

    Application of principles

    • Principles apply to process and product
    • Principles become practice through methods and techniques
      • often methods and techniques are packaged in a methodology
      • methodologies can be enforced by tools

    A visual representation

    Key principles

    • Rigor and formality
    • Separation of concerns
    • Modularity
    • Abstraction
    • Anticipation of change
    • Generality
    • Incrementality

    Rigor and formality

    • Software engineering is a creative design activity, BUT
    • It must be practiced systematically
    • Rigor is a necessary complement to creativity that increases our confidence in our developments
    • Formality is rigor at the highest degree
      • software process driven and evaluated by mathematical laws

    Examples: product

    • Mathematical (formal) analysis of program correctness
    • Systematic (rigorous) test data derivation

    Example: process

    • Rigorous documentation of development steps helps project management and assessment of timeliness

    Separation of concerns

    •  To dominate complexity, separate the issues to concentrate on one at a time
    • "Divide & conquer" (divide et impera)
    • Supports parallelization of efforts and separation of responsibilities

    Example: process

    • Go through phases one after the other (as in waterfall)
      • Does separation of concerns by separating activities with respect to time

    Example: product

    • Keep product requirements separate
      • functionality
      • performance
      • user interface and usability


    • A complex system may be divided into simpler pieces called modules
    • A system that is composed of modules is called modular
    • Supports application of separation of concerns
      • when dealing with a module we can ignore details of other modules

    Cohesion and coupling

    • Each module should be highly cohesive
      • module understandable as a meaningful unit
      • Components of a module are closely related to one another
    • Modules should exhibit low coupling
      • modules have low interactions with others
      • understandable separately

    A visual representation


    • Identify the important aspects of a phenomenon and ignore its details
    • Special case of separation of concerns
    • The type of abstraction to apply depends on purpose
    • Example : the user interface of a watch (its buttons) abstracts from the watch's internals for the purpose of setting time; other abstractions needed to support repair

    Abstraction ignores details

    • Example: equations describing complex circuit (e.g., amplifier) allows designer to reason about signal amplification
    • Equations may approximate description, ignoring details that yield negligible effects (e.g., connectors assumed to be ideal)

    Abstraction yields models

    • For example, when requirements are analyzed we produce a model of the proposed application
    • The model can be a formal or semiformal description
    • It is then possible to reason about the system by reasoning about the model

    An example

    • Programming language semantics described through an abstract machine that ignores details of the real machines used for implementation
      • abstraction ignores details such as precision of number representation or addressing mechanisms

    Abstraction in process

    • When we do cost estimation we only take some key factors into account
    • We apply similarity with previous systems, ignoring detail differences

    Anticipation of change

    • Ability to support software evolution requires anticipating potential future changes
    • It is the basis for software evolvability
    • Example: set up a configuration management environment for the project (as we will discuss)


    • While solving a problem, try to discover if it is an instance of a more general problem whose solution can be reused in other cases
    • Carefully balance generality against performance and cost
    • Sometimes a general problem is easier to solve than a special case


    • Process proceeds in a stepwise fashion (increments)
    • Examples (process)
      • deliver subsets of a system early to get early feedback from expected users, then add new features incrementally
      • deal first with functionality, then turn to performance
      • deliver a first prototype and then incrementally add effort to turn prototype into product

    Case study: compiler

    • Compiler construction is an area where systematic (formal) design methods have been developed
      • e.g., BNF for formal description of language syntax

    Separation of concerns example

    • When designing optimal register allocation algorithms (runtime efficiency) no need to worry about runtime diagnostic messages (user friendliness)


    • Compilation process decomposed into phases
      • Lexical analysis
      • Syntax analysis (parsing)
      • Code generation
    • Phases can be associated with modules

    Representation of modular structure

    boxes represent modules
    directed lines represent interfaces

    Module decomposition may be iterated

    further modularization of code-generation module


    • Applied in many cases
      • abstract syntax to neglect syntactic details such as begin…end vs. {…} to bracket statement sequences
      • intermediate machine code (e.g., Java Bytecode) for code portability

    Anticipation of change

    • Consider possible changes of
      • source language (due to standardization committees)
      • target processor
      • I/O devices


    • Parameterize with respect to target machine (by defining intermediate code)
    • Develop compiler generating tools (compiler compilers) instead of just one compiler


    • Incremental development
      • deliver first a kernel version for a subset of the source language, then increasingly larger subsets
      • deliver compiler with little or no diagnostics/optimizations, then add diagnostics/optimizations

    Case study (system engineering): elevator system

    • In many cases, the "software engineering" phase starts after understanding and analyzing the "systems engineering” issues
    • The elevator case study illustrates the point

    Rigor & formality

    • Quite relevant: it is a safety critical system
      • Define requirements
        • must be able to carry up to 400 Kg. (safety alarm and no operation if overloaded)
        • emergency brakes must be able to stop elevator within 1 m. and 2 sec. in case of cable failures
      • Later, verify their fulfillment

    Separation of concerns

    • Try to separate
      • safety
      • performance
      • usability (e.g, button illumination)
      • cost
    • although some are strongly related
      • cost reduction by using cheap material can make solution unsafe

    A modular structure

    Module decomposition may be iterated


    • The modular view we provided does not specify the behavior of the mechanical and electrical components
      • they are abstracted away

    Anticipation of change, generality

    • Make the project parametric wrt the number of elevators (and floor buttons)


    • What is design 
    • How can a system be decomposed into modules 
    • What is a module’s interface
    • What are the main relationships among modules
    • Prominent software design techniques and information hiding
    • The UML collection of design notations
    • Design of concurrent and distributed software 
    • Design patterns
    • Architectural styles
    • Component based software engineering

    What is design?

    • Provides structure to any artifact
    • Decomposes system into parts, assigns responsibilities, ensures that parts fit together to achieve a global goal
    • Design refers to both an activity and the result of the activity

    Two meanings of "design" activity in our context

    • Activity that acts as a bridge between requirements and the implementation of the software 
    • Activity that gives a structure to the artifact 
      • e.g., a requirements specification document must be designed
        • must be given a structure that makes it easy to understand and evolve

    The sw design activity

    • Defined as system decomposition into modules
    • Produces a Software Design Document
      • describes system decomposition into modules
    • Often a software architecture is produced prior to a software design

    Software architecture

    • Shows gross structure and organization of the system to be defined
    • Its description includes description of 
      • main components of a system
      • relationships among those components
      • rationale for decomposition into its components
      • constraints that must be respected by any design of the components
    • Guides the development of the design

    Two important goals

    • Design for change (Parnas)
      • designers tend to concentrate on current needs
      • special effort needed to anticipate likely changes
    • Product families (Parnas)
      • think of the current system under design as a member of a program family

    Sample likely changes?

    • Algorithms
      • e.g., replace inefficient sorting algorithm with a more efficient one
    • Change of data representation
      • e.g., from binary tree to a threaded tree (see example)
      • ≡17% of maintenance costs attributed to data representation changes (Lientz and Swanson, 1980)


    Sample likely changes? (cont')

    • Change of underlying abstract machine
      • new release of operating system
      • new optimizing compiler
      • new version of DBMS
    • Change of peripheral devices
    • Change of "social" environment
      • new tax regime
      • EURO vs national currency in EU
    • Change due to development process (transform prototype into product)

    Product families

    • Different versions of the same system
      • e.g. a family of mobile phones
        • members of the family may differ in network standards, end-user interaction languages, …
      • e.g. a facility reservation system
        • for hotels: reserve rooms, restaurant, conference space, …, equipment (video beamers, overhead projectors, …)
        • for a university
          • many functionalities are similar, some are different (e.g., facilities may be free of charge or not)

    Design goal for family

    • Design the whole family as one system, not each individual member of the family separately

    Sequential completion: the wrong way

    • Design first member of product family
    • Modify existing software to get next member products

    Sequential completion: a graphical view

    How to do better

    • Anticipate definition of all family members
    • Identify what is common to all family members, delay decisions that differentiate among different members
    • We will learn how to manage change in design


    • A well-defined component of a software system
    • A part of a system that provides a set of services to other modules
      • Services are computational elements that other modules may use


    • How to define the structure of a modular system?
    • What are the desirable properties of that structure?

    Modules and relations

    • Let S be a set of modules 
      S = {M1, M2, . . ., Mn}
    • A binary relation r on S is a subset of
      S x S
    • If Mi and Mj are in S, <Mi, Mj> r can be written as Mi r Mj


    • Transitive closure r+ of r 
      Mi r+ Mj iff Mi r Mj or ∃ Mk in S s.t. Mi r Mk and Mk r+ Mj
      (We assume our relations to be irreflexive)
    • r is a hierarchy iff there are no two elements Mi, Mj s.t. Mi r+ Mj Λ Mj r+ Mi

    Relations (cont')

    • Relations can be represented as graphs
    • A hierarchy is a DAG (directed acyclic graph)
    • a graph
    • a DAG

    The USES relation

    • A uses B
      • A requires the correct operation of B
      • A can access the services exported by B through its interface
      • it is “statically” defined
      • A depends on B to provide its services
        • example: A calls a routine exported by B
    • A is a client of B; B is a server

    Desirable property

    • USES should be a hierarchy
    • Hierarchy makes software easier to understand
      • we can proceed from leaf nodes (who do not use others) upwards
    • They make software easier to build
    • They make software easier to test


    • Organizes the modular structure through levels of abstraction
    • Each level defines an abstract (virtual) machine for the next level
      • level can be defined precisely
        • Mi has level 0 if no Mj exists s.t. Mi r Mj
        • let k be the maximum level of all nodes Mj s.t. Mi r Mj. Then Mi has level k+1


    • Used to describe a higher level module as constituted by a number of lower level modules
      • B consists of several modules, of which one is A
    • we say that Ms,i IMPLEMENTS Mi
      \[ {M_{S,i}}={{M_{k}}|{M_{k}}\epsilon S \Lambda {M_{k}} IsComponentOf {M_{i}}} \]

    A graphical view

                                                              They are a hierarchy

    Product families

    • Careful recording of (hierarchical) USES relation and IS_COMPONENT_OF supports design of program families

    Interface vs. implementation

    • To understand the nature of USES, we need to know what a used module exports through its interface
    • The client imports the resources that are exported by its servers
    • Modules implement the exported resources
    • Implementation is hidden to clients
    • Clear distinction between interface and implementation is a key design principle
    • Supports separation of concerns
      • clients care about resources exported from servers
      • servers care about implementation
    • Interface acts as a contract between a module and its clients

    Interface vs. implementation (cont')

    interface is like the tip of the iceberg

    Information hiding

    • Basis for design (i.e. module decomposition)
    • Implementation secrets are hidden to clients
    • They can be changed freely if the change does not affect the interface
    • Golden design principle
        • Try to encapsulate changeable design decisions as implementation secrets within module implementations

    How to design module interfaces?

    • Example: design of an interpreter for language MINI
      • We introduce a SYMBOL_TABLE module
        • provides operations to 
          • CREATE an entry for a new variable 
          • GET the value associated with a variable
          • PUT a new value for a given variable
    • the module hides the internal data structure of the symbol table
    • the data structure may freely change without affecting clients

    Interface design

    • Interface should not reveal what we expect may change later
    • It should not reveal unnecessary details
    • Interface acts as a firewall preventing access to hidden parts


    • Once an interface is defined, implementation can be done 
      • first quickly but inefficiently
      • then progressively turned into the final version
    • Initial version acts as a prototype that evolves into the final product

    More on likely changes an example

    • Policies may be separated from mechanisms
      • mechanism
        • ability to suspend and resume tasks in a concurrent system
      • policy
        • how do we select the next task to resume?
          • different scheduling policies are available
          • they may be hidden to clients
          • they can be encapsulated as module secrets

    Design notations

    • Notations allow designs to be described precisely
    • They can be textual or graphic
    • We illustrate two sample notations 
      • TDN (Textual Design Notation)
      • GDN (Graphical Design Notation)
    • We discuss the notations provided by UML

    TDN & GDN

    • Illustrate how a notation may help in documenting design
    • Illustrate what a generic notation may look like
    • Are representative of many proposed notations
    • TDN inherits from modern languages, like Java, Ada, …

    An example

    Comments in TDN

    • May be used to specify the protocol to be followed by the clients so that exported services are correctly provided
      • e.g., a certain operation which does the initialization of the module should be called before any other operation
      • e.g., an insert operation cannot be called if the table is full

    Example (cont')


    • Notation helps describe a design precisely
    • Design can be assessed for consistency
      • having defined module X, modules R and T must be defined eventually
        • if not → incompleteness
      • R, T replace X 
        • → either one or both must use Y, Z

    Example: a compiler

    module COMPILER
    exports procedure MINI (PROG: in file of char;
                    CODE: out file of char);
        MINI is called to compile the program stored in PROG
        and produce the object code in file CODE implementation
        A conventional compiler implementation.
        ANALYZER performs both lexical and syntactic analysis
        and produces an abstract tree, as well as entries in the
        symbol table; CODE_GENERATOR generates code
        starting from the abstract tree and information stored
        in the symbol table. MAIN acts as a job coordinator. is composed of ANALYZER, SYMBOL_TABLE,     ABSTRACT_TREE_HANDLER, CODE_GENERATOR, MAIN
    end COMPILER

    Other modules

    module MAIN uses ANALYZER, CODE_GENERATOR exports procedure MINI (PROG: in file of char;
                    CODE: out file of char);

    end MAIN

    module ANALYZER uses SYMBOL_TABLE, ABSTRACT_TREE_HANDLER exports procedure ANALYZE (SOURCE: in file of char);
        SOURCE is analyzed; an abstract tree is produced
        by using the services provided by the tree handler,
        and recognized entities, with their attributes, are
        stored in the symbol table.
    end ANALYZER

    Other modules (cont')

    exports procedure CODE (OBJECT: out file of char);
        The abstract tree is traversed by using the
        operations exported by the
        ABSTRACT_TREE_HANDLER and accessing
        the information stored in the symbol table
        in order to generate code in the output file.

    GDN description of module X

    X's decomposition

    Categories of modules

    • Functional modules
      • traditional form of modularization
      • provide a procedural abstraction
      • encapsulate an algorithm
        • e.g. sorting module, fast Fourier transform module, …

    Categories of modules (cont')

    • Libraries
      • a group of related procedural abstractions
        • e.g., mathematical libraries
          • implemented by routines of programming languages
    • Common pools of data
      • data shared by different modules
        • e.g., configuration constants
          • the COMMON FORTRAN construct

    Categories of modules (cont')

    • Abstract objects
      • Objects manipulated via interface functions
      • Data structure hidden to clients
    • Abstract data types
      • Many instances of abstract objects may be generated

    Abstract objects: an example

    • A calculator of expressions expressed in Polish postfix form
    • a*(b+c) → abc+*
    • a module implements a stack where the values of operands are shifted until an operator is encountered in the expression
      (assume only binary operators)

    Example (cont')

    • Interface of the abstract object STACK

      procedure PUSH (VAL: in integer);
      procedure POP_2 (VAL1, VAL2: out integer);

    Design assessment

    • How does the design anticipate change in type of expressions to be evaluated?
      • e.g., it does not adapt to unary operators

    Abstract data types (ADTs)

    • A stack ADT


    • Correspond to Java and C++ classes
    • Concept may also be implemented by Ada private types and Modula-2 opaque types
    • May add notational details to specify if certain built-in operations are available by default on instance objects of the ADT
      • e.g., type A_TYPE: ? (:=, =) indicates that assignment and equality check are available

    An example: simulation of a gas station

    module FIFO_CARS
    uses CARS
        type QUEUE : ?;
        procedure ENQUEUE (Q: in out QUEUE ; C: in CARS);
        procedure DEQUEUE (Q: in out QUEUE ; C: out CARS);
        function IS_EMPTY (Q: in QUEUE) : BOOLEAN;
        function LENGTH (Q: in QUEUE) : NATURAL;
        procedure MERGE (Q1, Q2 : in QUEUE ; Q : out QUEUE);
        This is an abstract data-type module representing
        queues of cars, handled in a strict FIFO way;
        queues are not assignable or checkable for equality,
        since “:=” and “=” are not exported.
    end FIFO_CARS

    Generic modules (templates)

    • They are parametric wrt a type

          generic module GENERIC_STACK_2
              . . .
              procedure PUSH (VAL : in T);   
              procedure POP_2 (VAL1, VAL2 : out T);
          end GENERIC_STACK_2


    • Possible syntax:

    More on genericity

    • How to specify that besides a type also an operation must be provided as a parameter
      generic module M (T) with OP(T)
      uses ...
      end M
    • Instantiation
      module M_A_TYPE is M(A_TYPE) PROC(M_A_TYPE)

    Specific techniques for design for change

    • Use of configuration constants
      • factoring constant values into symbolic constants is a common implementation practice
        • e.g., #define in C
          #define MaxSpeed 5600;

    Specific techniques for design for change (cont')

    • Conditional compilation
      ...source fragment common to all versions...
      # ifdef hardware-1
      ...source fragment for hardware 1 ...
      # endif
      #ifdef hardware-2
      ...source fragment for hardware 2 ...
      # endif
    • Software generation
      • e.g., compiler compilers (yacc, interface prototyping tools)

    Stepwise refinement

    • A systematic, iterative program design technique that unfortunately may lead to software that is hard to evolve 
    • At each step, problem P decomposed into
      • sequence of subproblems: P1; P2; …Pn
      • a selection: if (cond) then P1 else P2
      • an iteration: while (cond) do_something

    Example derivation of selection sort

    Step 1
        let n be the length of the array a to be sorted;
        i := 1 ;
        while i < n loop
            find the  smallest of ai .. .an, and exchange
            it with the element at position i;
            i := i + 1;

        end loop;

    Step 2
            let n be the length of the array a to be sorted;
            i := 1 ;
            while i < n loop
                j := n;
                while j > i loop
                    if a(i) > a(j) then
                        interchange the elements at positions j and i ;
                    end if;
                    j := j - 1;
                end loop;
                i := i + 1;
            end loop;

    Example derivation of selection sort (cont')

    Step 3
            let n be the length of the array a to be sorted;
            i := 1 ;
            while i < n loop
                j := n;
                while j > i loop
                    if a(i) > a(j) then
                        x := a(i);
                        a(i) := a(j);
                        a(j) := x;
                    end if;
                    j := j - 1;
                end loop;
                i := i + 1;
            end loop; 

    Decomposition tree

    • Stepwise refinement process may be depicted by a decomposition tree (DT)
      • root labeled by name of top problem
      • subproblem nodes labeled as children of parent node corresponding to problem
      • children from left to right represent sequential order of execution
      • if and while nodes denoted by suitable decoration


    Step 1
            P;        P problem to solve
    Step 2
            P1; P2; P3;    P decomposed into sequence    
    Step 3
            while C loop
                P2,1;    P2  decomposed into a loop    
            end loop;       
    Step 4
            while C loop
                if C1 then P2,1 decomposed into selection
                end if;
            end loop;

    Corresponding DT

    Relation with IS_COMPOSED_OF

    • Let M, M1, M2, M3 be modules representing P, P1, P2, P3
    • We cannot write
      • M IS_COMPOSED_OF {M1,M2,M3}
    • We need to add further module acting as glue to impose a sequential flow from M1 to M2 to M3

    An assessment of stepwise refinement

    • Stepwise refinement is a programming technique, not a modularization technique
    • When used to decompose system into modules, it tends to analyze problems in isolation, not recognizing commonalities
    • It does not stress information hiding

    An assessment of stepwise refinement (cont')

    • No attention is paid to data (it decomposes functionalities)
    • Assumes that a top function exists
      • but which one is it in the case of an operating system? or a word processor?
    • Enforces premature commitment to control flow structures among modules

    Example a program analyzer

    Step 1
        Recognize a program stored in a given file f;
    Step 2
        correct := true;
        analyze f according to the language definition;
        if correct then
            print message "program correct";
            print message "program incorrect";
        end if;

    Example a program analyzer (cont')

    Step 3
        correct := true;
        perform lexical analysis:
            store program as token sequence  in file ft
            and symbol table in file fs, and set error_in_lexical_phase
        if error_in_lexical_phase then
            correct := false;
            perform syntactic analysis and set Boolean variable
            error_in_syntactic_phase accordingly:
            if error_in_syntactic_phase then
                correct := false;
            end if;
        end if;
        if correct then
            print message "program correct";
            print message "program incorrect";
        end if;


    • Two passes
      • Lexical analysis comes first on the entire program, producing two files
    • What if we want to switch to a process driven by syntax analysis (it requests the lexical analyzer to provide a token when needed)
      • everything changes!!!

    A better design based on information hiding

    • Module CHAR_HOLDER
      • hides physical representation of input file 
      • exports operation to access source file on a character-by-character basis
    • Module SCANNER
      • hides details of lexical structure of the language 
      • exports operation to provide next token
    • Module PARSER
      • hides data structure used to perform syntactic analysis (abstract object PARSER)

    Top-down vs. bottom-up

    • Information hiding proceeds bottom-up
    • Iterated application of IS_COMPOSED_OF proceeds top-down
      • stepwise refinement is intrinsically top-down
    • Which one is best?
      • in practice, people proceed in both directions
        • yo-yo design
      • organizing documentation as a top-down flow may be useful for reading purposes, even if the process followed was not top-down

    Handling anomalies

    • Defensive design
    • A module is anomalous if it fails to provide the service as expected and as specified in its interface
    • An exception MUST be raised when anomalous state is recognized

    How can failures arise?

    • Module M should fail and raise an exception if 
      • one of its clients does not satisfy the required protocol for invoking one of M’s services
      • M does not satisfy the required protocol when using one of its servers, and the server fails
      • hardware generated exception (e.g., division by zero)

    What a module can do before failing

    • Before failing, modules may try to recover from the anomaly by executing some exception handler (EH)
      • EH is a local piece of code that may try to recover from anomaly (if successful, module does not fail)
      • or may simply do some cleanup of the module’s state and then let the module fail, signaling an exception to its client


    Example of exception propagation

    Case study

    • Compiler for the MIDI programming language
    • The language is block-structured
    • It requires a symbol table module that can cope with block static nesting
    • We discuss here module SYMBOL_TABLE

    SYMBOL_TABLE (vers.1)

    Version 1 is not robust

    • Defensive design should be applied
    • Exceptions must be raised in these cases:
      • INSERT: insertion cannot be done because identifier with same name already exists in current scope
      • RETRIEVE and LEVEL: identifier with specified name not visible
      • ENTER_SCOPE: maximum nesting depth exceeded
      • EXIT_SCOPE: no matching block entry exists

    SYMBOL_TABLE (vers.2)

    SYMBOL_TABLE uses a list management module

    Concurrent software

    • The case of a module defining shared data
    • E.g., abstract object BUFFER
      with operations
      • PUT: inserts a character in BUFFER
      • GET: extracts a character from BUFFER 
      • NOT_FULL: returns true if BUFFER not full 
      • NOT_EMPTY: returns true if BUFFER not empty

    How to control correct access to shared data?

    • Not sufficient that clients check operation invocations, such as 

      end if; 
    • Consumer_1 and Consumer_2 might do this concurrently
      • if only one slot is left, both may find the buffer not full, the first who writes fills it, and the other writes in a full buffer

    Enforcing synchronization

    • Ensure that operations on buffer are executed in mutual exclusion
    • Ensure that operations such as

      end if;

      are executed as logically non-interruptible units


    • Abstract objects used in a concurrent environment
    • Available in the Java programming language

    Monitors: an example


    • Monitor operations are assumed to be executed in mutual exclusion
    • A requires clause may be associated with an operation
      • it is automatically checked when operation is called
      • if the result is false, the current process is suspended until it becomes true (at that stage it becomes eligible for resumption)

    Monitor types: an example

    Guardians and rendez-vous

    • The Ada style of designing concurrent systems
    • In Ada a shared object is active (whereas a monitor is passive)
      • it is managed by a guardian process which can accept rendez-vous requests from tasks willing to access the object

    A guardian task

    note nondeterministic acceptance of rendez-vous requests

    Real-time software

    • Case where processes interact with the environment
    • E.g., a put operation on a shared buffer is invoked by a plant sensor sending data to a controller
      • plant cannot be suspended if buffer full!
        • design must ensure that producer never finds the buffer full
          • this constrains the speed of the consumer process in the controller

    TDN description

    GDN description

    zig-zag arrow indicates asynchronous invocation

    Distributed software

    • Issues to consider
      • module-machine binding
      • intermodule communication
        • e.g., remote procedure call or message passing
      • access to shared objects
        • may require replication for efficiency reasons

    Client-server architecture

    • The most popular distributed architecture
    • Server modules provide services to client modules
    • Clients and servers may reside on different machines


    • Binding modules to machines
      • static vs. dynamic (migration)
    • Inter-module communication
      • e.g., RPC
      • IDL to define interface of remote procedures
    • Replication and distribution


    • Layer residing between the network operating system and the application
    • Helps building network applications
    • Provides useful services
      • Name services, to find processes or resources on the network
      • Communication services, such as message passing or RPC (or RMI)

    Object-oriented design

    • One kind of module, ADT, called class
    • A class exports operations (procedures) to manipulate instance objects
      • often called methods
    • Instance objects accessible via references

    Syntactic changes in TDN

    • No need to export opaque types
      • class name used to declare objects
    • If a is a reference to an object
      • a.op (params);

    A further relation: inheritance

    • ADTs may be organized in a hierarchy
    • Class B may specialize class A
      • B inherits from A
        conversely, A generalizes B
    • A is a superclass of B
    • B is a subclass of A

    An example

    An example (cont’)


    • A way of building software incrementally
    • A subclass defines a subtype
      • subtype is substitutable for parent type
    • Polymorphism
      • a variable referring to type A can refer to an object of type B if B is a subclass of A
    • Dynamic binding 
      • the method invoked through a reference depends on the type of the object associated with the reference at runtime

    How can inheritance be represented?

    • We start introducing the UML notation
    • UML (Unified Modeling Language) is a widely adopted standard notation for representing OO designs
    • We introduce the UML class diagram
      • classes are described by boxes

    UML representation of inheritance

    UML associations

    • Associations are relations that the implementation is required to support
    • Can have multiplicity constraints


    • Defines a PART_OF relation
      Differs from IS_COMPOSED_OF
      Here TRANGLE has its own methods
      It implicitly uses POINT to define 
      its data attributes

    More on UML

    • Representation of IS_COMPONENT_OF via the package notation

    Software architecture

    • Describes overall system organization and structure in terms of its major constituents and their interactions 
    • Standard architectures can be identified
      • pipeline
      • blackboard
      • event based (publish-subscribe)

    Standard architectures

    Domain specific architectures

    • "model–view–controller" architecture for software that has a significant amount of user interaction 

    Software components

    • Goal
      • build systems out of pre-existing libraries of components
      • as most mature engineering areas do
    • Examples
      • STL for C++
      • JavaBeans and Swing for Java

    Component integration

    • The CORBA (Common Object Request Broker Architecture) Middleware
    • Clients and servers connected via an Object Request Broker (ORB)
    • Interfaces provided by servers defined by an Interface Definition Language (IDL)
    • In the Microsoft world: DCOM (Distributed Component Object Model)

    The CORBA architecture

    Architectures for distributed systems

    • From two tiered
      • Client-server
    • to three tiered


    • Introduction
    • Types of specifications
      • operational 
        • Data Flow Diagrams
        • (Some) UML diagrams
        • Finite State Machines
        • Petri Nets 
      • descriptive
        • Entity Relationship Diagrams
        • Logic-based notations
        • Algebraic notations
    • Languages for modular specifications 
      • Statecharts
      • Z


    • A broad term that means definition
    • Used at different stages of software development for different purposes
    • Generally, a statement of agreement (contract) between
      • producer and consumer of a service
      • implementer and user
    • All desirable qualities must be specified

    Uses of specification

    • Statement of user requirements
      • major failures occur because of misunderstandings between the producer and the user 
      • "The hardest single part of building a softwarem system is deciding precisely what to build" (F. Brooks)
    • Statement of the interface between the machine and the controlled environment 
      • serious undesirable effects can result due to misunderstandings between software engineers and domain experts about the phenomena affecting the control function to be implemented by software

    Uses of specification (cont')

    • Statement of requirements for implementation
      • design process is a chain of specification (i.e., definition)–implementation–verification steps 
        • requirements specification refers to definition of external behavior
          • design specification must be verified against it
        • design specification refers to definition of the software architecture
          • code must be verified against it
    • A reference point during maintenance
      • corrective maintenance only changes implementation
      • adaptive and perfective maintenance occur because of requirements changes
        • requirements specification must change accordingly

    Specification qualities

    • Precise, clear, unambiguous
    • Consistent
    • Complete 
      • internal completeness
      • external completeness
    • Incremental

    Clear, unambiguous, understandable

    • Example: specification fragment for a word-processor

      Selecting is the process of designating areas of the document that you want to work on. Most editing and formatting actions require two steps: first you select what you want to work on, such as text or graphics; then you initiate the appropriate action. 

      can an area be scattered?

    Precise, unambiguous, clear

    • Another example (from a real safety-critical system)

      The message must be triplicated. The three copies must be forwarded through three different physical channels. The receiver accepts the message on the basis of a two-out-of-three voting policy. 

      can a message be accepted as soon as we receive 2 out of 3 identical copies of message or do we need to wait for receipt of the 3rd?


    • Example: specification fragment for a word-processor

      The whole text should be kept in lines of equal length. The length is specified by the user. Unless the user gives an explicit hyphenation command, a carriage return should occur only at the end of a word.

      What if the length of a word exceeds the length of the line?


    • Internal completeness
      • the specification must define any new concept or terminology that it uses
        • glossary helpful for this purpose 
      • the specification must document all the needed requirements
        • difficulty: when should one stop?


    • Referring to the specification process
      • start from a sketchy document and progressively add details
    • Referring to the specification document
      • document is structured and can be understood in increments

    Classification of specification styles

    • Informal, semi-formal, formal
    • Operational
      • Behavior specification in terms of some abstract machine
    • Descriptive
      • Behavior described in terms of properties

    Example 1

    • Specification of a geometric figure E:

      E can be drawn as follows:
      1. Select two points P1 and P2 on a plane
      2. Get a string of a certain length and fix its ends to P1 and P2
      3. Position a pencil as shown in next figure
      4. Move the pen clockwise, keeping the string tightly stretched, until you reach the point where you started drawing

      this is an operational specification

    A descriptive specification

    • Geometric figure E is describe by the following equation
      ax2 + by2 + c = 0
      where a, b, and c are suitable constants

    Another example

    “Let a be an array of n elements. The result of its sorting is an array b of n elements such that the first element of b is the minimum of a (if several elements of a have the same value, any one of them is acceptable); the second element of b is the minimum of the array of n-1 elements obtained from a by removing its minimum element; and so on until all n elements of a have been removed.”
    “The result of sorting array a is an array b which is a permutation of a and is sorted.”

    How to verify a specification?

    • “Observe” dynamic behavior of specified system (simulation, prototyping, “testing” specs)
    • Analyze properties of the specified system
    • Analogy with traditional engineering
      • physical model of a bridge
      • mathematical model of a bridge

    Data Flow Diagrams (DFDs)

    • A semi-formal operational specification
    • System viewed as collection of data manipulated by “functions”
    • Data can be persistent
      • they are stored in data repositories
    • Data can flow 
      • they are represented by data flows
    • DFDs have a graphical notation

    Graphical notation

    • bubbles represent functions
    • arcs represent data flows
    • open boxes represent persistent store
    • closed boxes represent I/O interaction


    • specifies evaluation of (a + b) * (c + a * d) 

    A construction “method” (1)

    • 1. Start from the “context” diagram

    A construction “method” (2)

    • 2. Proceed by refinements until you reach “elementary” functions (preserve balancing)

    A library example

    Refinement of“Get a book”

    Patient monitoring systems

    The purpose is to monitor the patients’ vital factors--blood, pressure, temperature, …--reading them at specified frequencies from analog devices and storing readings in a DB. If readings fall outside the range specified for patient or device fails an alarm must be sent to a nurse. The system also provides reports.

    A refinement

    More refinement

    An evaluation of DFDs

    • Easy to read, but …
    • Informal semantics
      • How to define leaf functions?
      • Inherent ambiguities
    • Outputs from A, B, C are all needed?
    • Outputs for E and F are produced at the same time?

    An evaluation of DFDs (cont')

    • Control information is absent
    • Possible interpretations:
      • A produces datum, waits until B consumes it
      • B can read the datum many times without consuming it
      • a pipe is inserted between A and B


    • There have been attempts to formalize DFDs
    • There have been attempts to extend DFDs (e.g., for real-time systems)

    UML use-case diagrams

    • Define functions on basis of actors and actions

    UML sequence diagrams

    • Describe how objects interact by exchanging messages
    • Provide a dynamic view

    UML collaboration diagrams

    • Give object interactions and their order
    • Equivalent to sequence diagrams

    Finite state machines (FSMs)

    • Can specify control flow aspects
    • Defined as
      a finite set of states, Q;
      a finite set of inputs, I;
      a transition function d : Q x I → Q
      (d can be a partial function)

    Example: a lamp

    Another example:a plant control system

    A refinement

    Classes of FSMs

    • Deterministic/nondeterministic
    • FSMs as recognizers
      • introduce final states
    • FSMs as transducers
      • introduce set of outputs
    • . . .

    FSMs as recognizers

    qf is a final state

    FSMs as recognizers


    • Finite memory
    • State explosion
      • Given a number of FSMs with k1, k2, … kn states, their composition is a FSM with k1 * k2 *… * kn. This growth is exponential with the number of FSMs, not linear (we would like it to be k1 + k2 +… + kn )

    State explosion: an example

    The resulting FSM

    Petri nets

    • A quadruple (P,T,F,W)
      P: places T: transitions (P, T are finite) 
      F: flow relation (F ⊆ {P x T} U {T x P} ) W: weight function (W: F → N – {0} )

      (1) P Π T = Ø
      (2) P U T ≠ Ø
      (3)F ⊆ (P x T) U (T x P)
      (4) W: F → N - {0}

      Default value of W is 1

      State defined by marking: M: P → N

    Graphical representation

    Semantics: dynamic evolution

    • Transition t is enabled iff
      • ∀p ∈ t's input places, M(p) ≥ W(<p,t>)
    • t fires: produces a new marking M’ in places that are either t's input or output places or both
      • if p is an input place: M'(p) = M(p) - W(<p,t>)
      • if p is an output place: M'(p) = M(p) + W(<t,p>)
      • if p is both an input and an output place: M'(p) = M(p) - W(<p,t>) + W(<t,p>)


    • Any of the enabled transitions may fire
    • Model does not specify which fires, nor when it fires

    Modeling with Petri nets

    • Places represent distributed states
    • Transitions represent actions or events that may occur when system is in a certain state
    • They can occur as certain conditions hold on the states

    Common cases

    • Concurrency
      • two transitions are enabled to fire in a given state, and the firing of one does nor prevent the other from firing 
        • see t1 and t2 in case (a)
    • Conflict
      • two transitions are enabled to fire in a given state, but the firing of one prevents the other from firing
        • see t3 and t4 in case (d)
        • place P3 models a shared resource between two processes
      • no policy exists to resolve conflicts (known as unfair scheduling)
      • a process may never get a resource (starvation)

    How to avoid starvation

    imposes alternation

    A conflict-free net

    this net can deadlock! consider <t1,t3',t2,t4'>

    A deadlock-free net

    A case of partial starvation

    Producer-consumer example (1)

    Producer-consumer example (2)

    Limitations and extensions

    Token represents a message.

    You wish to say that the delivery channel depends on contents.


    Petri nets cannot specify selection policies.

    Extension 1 assigning values to tokens

      • Transitions have associated predicates and functions
      • Predicate refers to values of tokens in input places selected for firing
      • Functions define values of tokens produced in output places


      • Predicate P2 > P1 and function P4 := P2 + P1 associated with t1
      • Predicate P3 = P2 and functions P4 := P3  P2 and P5 := P2 + P3 are associated with t2 
      • The firing of t1 by using <3,7> would produce the value 10 in P4. t2 can then fire using <4, 4>

      Extension 2 specifying priorities

      • A priority function pri from transitions to natural numbers:
      • pri: T → N
      • When several transitions are enabled, only the ones with maximum priority are allowed to fire
      • Among them, the one to fire is chosen nondeterministically

      Extension 3 Timed Petri nets

      • A pair of constants is associated with each transition 
      • Once a transition is enabled, it must wait for at least tmin to elapse before it can fire
      • If enabled, it must fire before tmax has elapsed, unless it is disabled by the firing of another transition before tmax

      Example combining priorities and time

      Example combining priorities and time (cont')

      Example combining priorities and time (cont')

      Case study

      • An n elevator system to be installed in a building with m floors
      • Natural language specs contain several ambiguities
      • Formal specification using PNs removes ambiguities
      • Specification will be provided in a stepwise fashion
      • Will use modules, each encapsulating fragments of PNs which describe certain system components

      From informal specs…

      • “The illumination is cancelled when the elevator visits the floor and is either moving in the desired direction, or ...”
      • 2 different interpretations (case of up call)
        • switch off as the elevator arrives at the floor from below (obvious restrictions for 1st and last floor)
        • switch off after the elevators starts moving up
          • in practice you may observe the two cases!

      …more analysis of informal specs

      • “The algorithm to decide which to service first should minimize the waiting time for both requests.”
      • what does this mean?
        • in no other way can you satisfy either request in a shorter time
          • but minimizing for one may require longer for the other
        • the sum of both is minimal
          • why the sum?

      Initial sketch of movement

      Button module

      Elevator position (sketch)

      More precise description of elevator position

      Switch internal button off

      Switch external button off

      Specifying policy

      A “fair” solution:
          Keep the direction unchanged as long as there are
          calls that require elevator to go in that direction

      A general scheduler

      • Each transition has predicate OK(Scheduler)
      • Token in SCHEDULER stores information about the state of the system that is useful for scheduling transitions to fire 
      • The token is “permanent” (it is always reproduced after the firing of any transition)

      Declarative specifications

      • ER diagrams: semiformal specs
      • Logic specifications
      • Algebraic specifications

      ER diagrams

      • Often used as a complement to DFD to describe conceptual data models
      • Based on entities, relationships, attributes
      • They are the ancestors of class diagrams in UML



      • Relations can be partial
      • They can be annotated to define

        one to one

        one to many

        many to one

        many to many


      Non binary relations

      Logic specifications

      • Examples of first-order theory (FOT) formulas:

        x > y and y > z implies x > z
        x = y  Ξ  y = x
        for all x, y, z (x > y and y > z implies x > z)
        x + 1 < x – 1
        for all x (exists y (y = x + z))
        x > 3 or x < -6

      Specifying complete programs

      • A property, or requirement, for P is specified as a formula of the type
        {Pre (i1, i2,..., in) }
        {Post (o1, o2,..., om, i1, i2,..., in)}
        Pre: precondition
        Post: postcondition


      • Program to compute greatest common divisor
        {i1 > 0 and i2 > 0}
        {(exists z1, z2 (i1 = o * z1 and i2 = o * z2)
        and not (exists h 
        (exists z1, z2 (i1 = h * z1 and i2 = h * z2) and h > o))} 

      Specifying procedures

      {n > 0} -- n is a constant value

      procedure search (table: in integer_array; n: in integer;
      element: in integer; found: out Boolean);

      {found ≡ (exists i (1 ≤ i ≤ n and table (i) = element))

      {n > 0 } 

      procedure reverse (a: in out integer_array; n: in integer);

      {for all i (1 ≤ i ≤ n) implies (a (i) = old–a (n - i +1))}

      Specifying classes

      • Invariant predicates and pre/post conditions for each method
      • Example of invariant specifying an array implementing ADT set

        for all i, j (1 ≤ i ≤ length and 1 ≤ j ≤ length and i ≠ j) 
        implies IMPL[i] ≠ IMPL[j]
        (no duplicates are stored)

      Specifying non-terminating behaviors

      • Example: producer+consumer+buffer
      • Invariant specifies that whatever has been produced is the concatenation of what has been taken from the buffer and what is kept in the buffer

        input_sequence = append (output_sequence, contents(CHAR_BUFFER))

      A case-study using logic specifications

      • We outline the elevator example
      • Elementary predicates
        • at (E, F, T) 
          • E is at floor F at time T
        • start (E, F, T, up) 
          • E left floor F at time T moving up
      • Rules
        • (at (E, F, T) and on (EB, F1, T) and F1 > F) implies start (E, F, T, up)

      States and events

      • Elementary predicates are partitioned into
        • states, having non-null duration
          • standing(E, F, T1, T2)
            • assumption: closed at left, open at right
        • events
          • instantaneous (caused state change occurs at same time)
          • represented by predicates that hold only at a particular time instant
            • arrived (E, F, T)
      • For simplicity, we assume
        • zero decision time
        • no simultaneous events


      • arrival (E, F, T) 
        • E in [1..n], F in [1..m], T ≥ t0, (t0 initial time)
          • does not say if it will stop or will proceed, nor where it comes from
      • departure(E, F, D, T) 
        • E in [1..n], F in [1..m], D in {up, down}, T ≥ t0
      • stop (E, F, T)  
        • E in [1..n], F in [1.. m], T ≥ t0
          • specifies stop to serve an internal or external request

      Events (cont')

      • new_list (E, L, T) 
        • E in [1..n], L in [1.. m]*, T ≥ t0 
          • L is the list of floors to visit associated with elevator (scheduling is performed by the control component of the system)
      • call(F, D, T) 
        • external call (with restriction for 1, N)
      • request(E, F, T) 
        • internal reservation


      • moving (E, F, D, T1, T2)
      • standing (E, F, T1, T2)
      • list (E, L, T1, T2)
        • We implicitly assume that state predicates hold for any sub- interval (i.e., the rules that describe this are assumed to be automatically added)
          • Nothing prevents that it holds for larger interval

      Rules relating events and states

      R1: When E arrives at floor F, it continues to move if there is no request for service from F and the list is empty. If the floor to serve is higher, it moves upward; otherwise it moves downward.

      arrival (E, F, Ta) and
      list (E, L, T, Ta) and 
      first (L) > F
      departure (E, F, up, Ta)

      A similar rule describes downward movement.

      R2: Upon arrival at F, E stops if F must be serviced (F appears as first of the list)

      arrival (E, F, Ta) and
      list (E, L, T, Ta) and
      first (L) = F
      stop (E, F,Ta)

      R3: E stops at F if it gets there with an empty list

      arrival (E, F, Ta) and
      list (E, empty, T, Ta)
      stop (E, F, Ta)

      Rules relating events and states (cont')

      R4: Assume that elevators have a fixed time to service a floor. If the list is not empty at the end of such interval, the elevator leaves the floor immediately.

      stop (E, F, Ta) and
      list (E, L, T, Ta + Dts) and
      first (L) > F,
      departure (E, F, up, Ta + Dts

      R5: If the elevator has no floors to service, it stops until its list becomes nonempty.

      stop (E, F, Ta) and list (E, L, Tp, T) and
      Tp > Ta + Dts and list (E, empty, Ta + Dts, Tp) and
      first (L) > F
      departure (E, F, up, Tp)

      R6: Assume that the time to move from on floor to the next is known and fixed. The rule describes movement.

      departure (E, F, up, T)
      arrival (E, F + 1, T + Dt)

      Rules relating events and states (cont')

      R7: The event of stopping initiates standing for at least Dts.

      stop (E, F, T)
      standing (E, F, T, T + Dts)

      R8: At the end of the minimum stop interval Dts, E remains standing if there are no floors to service.

      stop (E, F, Ts) and
      list (E, empty, Ts + Dts, T)
      standing (E, F, Ts, T)

      R9: Departure causes moving.

      departure (E, F, D, T)
      moving (E, F, D, T, T + Dt)

      Control rules

      • Express the scheduling strategy (by describing “new_list”  events and “list” states)
      • Internal requests are inserted in the list from current floor to top if the elevator is moving up
      • External calls are inserted in the list of the closest eevator that is moving in the correct direction, or in a standing elevator

      Rules relating events and states (cont')

      R10: Reserving F from inside E, which is not standing at F, causes immediate update of L according to previous policy

      request (E, F, TR) and not (standing (E, F, Ta, TR)) and
      list (E, L, Ta, TR) and LF = insert_in_order(L, F, E)
      new_list (E, LF, TR)

      R11: Effect of arrival of E at floor F

      arrival (E, F, Ta) and list (E, L, T, Ta) and
      F = first (L) and Lt = tail (L)
      new_list (E, Lt, Ta)

      R12: How list changes

      new_list (E, L, T1) and not (new_list (E, L, T2) and
      T1 < T2 < T3)
      list (E, L, T1, T3)

      Verifying specifications

        • The system can be simulated by providing a state (set of facts) and using rules to make deductions
          • standing (2, 3, 5, 7) elevator 2 at floor 3 at least from instant 5 to 7
          • list(2, empty, 5, 7)
          • request(2, 8, 7)
          • new_list(2, {8}, 7)
        • (excluding other events)
          departure (2, up, 7 + Dts)
          arrival (2, 8, 7 + Dts + Dta *(8-3))
        • Properties can be stated and proved via deductions

          new_list (E, L, T) and F∈ L
          new_list (E, L1, T1) and F does not belongs to L1 and T1 > T2
          (all requests are served eventually)

        Descriptive specs

        • The system and its properties are described in the same language
        • Proving properties, however, cannot be fully mechanized for most languages

        Algebraic specifications

        • Define a heterogeneous algebra 
        • Heterogeneous = more than 1 set
        • Especially useful to specify ADTs


        • A system for strings, with operations for
          • creating new, empty strings (operation new)
          • concatenating strings (operation append)
          • adding a new character at the end of a string (operation add)
          • checking the length of a given string (operation length)
          • checking whether a string is empty (operation isEmpty)
          • checking whether two strings are equal (operation equal)

        Specification: syntax

        algebra StringSpec;
            sorts String, Char, Nat, Bool;
                new: () → String;
                append: String, String → String;
                add: String, Char → String;
                length: String → Nat;
                isEmpty: String → Bool;
                equal: String, String → Bool

        Specification: properties

        constrains new, append, add, length, isEmpty, equal so that
        for all [s, s1, s2: String; c: Char]
            isEmpty (new ()) = true;
            isEmpty (add (s, c)) = false;
            length (new ()) = 0;
            length (add (s, c)) = length (s) + 1;
            append (s, new ()) = s;
            append (s1, add (s2,c)) = add (append (s1,s2),c);
            equal (new (),new ()) = true;
            equal (new (), add (s, c)) = false;
            equal (add (s, c), new ()) = false;
            equal (add (s1, c), add (s2, c) = equal (s1,s2);
        end StringSpec. 

        Example: editor

        • newF
          • creates a new, empty file
        • isEmptyF
          • states whether a file is empty
        • addF
          • adds a string of characters to the end of a file
        • insertF
          • inserts a string at a given position of a file (the rest of the file will be rewritten just after the inserted string)
        • appendF
          • concatenates two files

        Example: editor (cont')

        algebra TextEditor;
            sorts Text, String, Char, Bool, Nat;
        newF: () →  Text;
        isEmptyF: Text → Bool;
        addF: Text, String → Text;
        insertF: Text, Nat, String → Text;
        appendF: Text, Text → Text;
        deleteF: Text → Text;
        lengthF : Text → Nat;
        equalF : Text, Text → Bool;
        addFC: Text, Char → Text;
                {This is an auxiliary operation that will be needed
                to define addF and other operations on files.}

        Example: editor (cont')

        constrains newF, isEmptyF, addF, appendF, insertF, deleteF
        so that TextEditor generated by [newF, addFC]
        for all [f, f1,f2: Text; s: String; c: Char; cursor: Nat]
            isEmptyF (newF ()) = true;
            isEmptyF (addFC (f, c)) = false;
            addF (f, newS ()) = f;
            addF (f, addS (s, c)) = addFC (addF (f, s), c);
            lengthF (newF ()) = 0;
            lengthF (addFC (f, c)) = lengthF (f) + 1;
            appendF (f, newF ()) = f;
            appendF (f1, addFC (f2, c)) =
                addFC (appendF (f1, f2), c);
            equalF (newF (),newF ()) = true;
            equalF (newF (), addFC (f, c)) = false;
            equalF (addFC (f, c), new ()) = false;
            equalF (addFC (f1, c1), addFC (f2, c2) =
            equalF (f1, f2) and equalC (c1, c2);
            insertF (f, cursor, newS ()) = f;
            ((equalF (f, appendF (f1, f2)) and (lengthF (f1) = cursor - 1))
            equalF (insertF (f, cursor, s), appendF (addF (f1, s), f2))) = true;
        end TextEditor.

        Requirements for a notation

        • Ability to support separation of concerns
          • e.g., separate functional specs from
            • performance specs 
            • user-interface specs
        • Support different views

        Example of views document production - data flow view (1)

        Control flow view (2)

        UML notations

        • Class diagrams
          • describe static architecture in terms of classes and associations
          • dynamic evolution can be described via Statecharts (see later)
        • Activity diagrams
          • describe sequential and parallel composition of method executions, and synchronization

        An activity diagram

        Building modular specifications

        • The case of algebraic specifications
          • How to combine algebras taken from a library
          • How to organize them in a hierarchy

        Algebras used by StringSpec

        algebra BoolAlg;
            sorts Bool;
                true () →  Bool;
                false () → Bool;
                not : Bool → Bool;
                and: Bool, Bool → Bool;
                or: Bool, Bool → Bool;
                implies: Bool, Bool → Bool;
                ≡ : Bool, Bool → Bool;
        constrains true, false, not, and, or, implies, ≡ so that
        Bool generated by [true, false]
        for all [a, b: Bool]
            not (true) = false;
            not (false) = true;
            a and b = not (not (a) or not (b));
            a implies b = not (a) or b;

        end BoolAlg.

        Algebras used by StringSpec (cont')

         algebra NatNumb;
            sorts Nat, Bool;
        0: () → Nat;
        Succ: Nat → Nat;
        + : Nat, Nat → Nat;
        - : Nat, Nat → Nat;
        = : Nat, Nat → Bool;

        constrains 0, Succ, +, -, =,..., so that
        NatNumb generated by [0, Succ]

        end NatNumb.
        algebra CharAlg;
            sorts Char, Bool;
                ‘a’: ()® Char;
                ‘b’ : ()® Char;
        end CharAlg.

        StringSpec revisited

        algebra StringSpec;
            imports BoolAlg, NatNumb, CharAlg;
                sorts String, Char, Nat, Bool;
                    new: () → String;
        end StringSpec. 

        Incremental specification of an ADT

        • We want to target stacks, queues, sets
        • We start from "container" and then progressively specialize it
        • We introduce another structuring clause
          • assumes
            • defines inheritance relation among algebras

        Container algebra

        algebra Container;
        imports DataType, BoolAlg, NatNumb;
            sorts Cont;
                new: () → Cont;
                insert: Cont, Data → Cont;
                    {Data is the sort of algebra DataType, to which
                    elements to be stored in Cont belong}
                isEmpty: Cont → Bool;
                size: Cont → Nat;
        constrains new, insert, isEmpty, size so that
        Cont generated by [new, insert]
        for all [d: Data; c: Cont]
            isEmpty (new ()) = true;
            isEmpty (insert (c, d)) = false;
            size (new ()) = 0;
        end Container.

        Table specializes Container

        algebra TableAlg;
        assumes Container;
            sorts Table;
                last: Table → Data;
                rest: Table → Table;
                equalT : Table, Table → Bool;
                delete: Table, Data → Table;
        constrains last, rest, equalT, delete, isEmpty, new, insert so that
        for all [d, d1, d2: Data; t, t1, t2: Table]
            last (insert (t, d)) = d;
            rest (new ()) = new ();
            rest (insert (t, d)) = t;
            equalT (new (), new ()) = true;
            equalT (insert (t, d), new ()) = false;
            equalT (new (), insert (t,d)) = false;
            equalT (t1,t2) = equalD(last (t1), last (t2)) and
            equalT (rest (t1),rest (t2));
            delete (new (), d) = new ();
            delete (insert (t,d),d) = delete (t, d);
            if not equalD(d1, d2) then
            delete (insert (t, d1), d2) = insert (delete (t, d2), d1);
        end TableAlg. 

        Queue specializes Container

        algebra QueueAlg;
        assumes Container;
            sort Queue;
                last: Queue → Data;
                first: Queue → Data;
                equalQ : Queue , Queue ® Bool;
                delete:Queue → Queue;
        constrains last, first, equalQ, delete, isEmpty, new, insert so that
        for all [d: Data; q, q1, q2: Queue]
            last (insert (q, d)) = d;
            first (insert (new(), d) = d
            first (insert (q, d)) = if not isEmpty (q) then first (q);
            equalQ (new (), new ()) = true;
            equalQ (insert (q, d), new ()) = false;
            equalQ (new (), insert (q, d)) = false;
            equalQ (insert (q1, d1), insert (q2, d2)) = equalD (d1, d2) and
            equalQ (q1,q2);
            delete (new ()) = new ();
            delete (insert (new (), d)) = new ();
            if not equalQ (q, new ()) then
            delete (insert (q,d)) = insert (delete (q), d);
        end QueueAlg. 

        A graphical view

        A richer hierarchy

        From specs to an implementation

        • Algebraic spec language described so far is based on the "Larch shared language"
        • Several "interface languages" are available to help transitioning to an implementation
          • Larch/C++, Larch/Pascal

        Using Larch/Pascal for StringSpec

        type String exports isEmpty, add, append,...
        based on Boolean, integer, character
            function isEmpty (s: String) : Boolean
                modifies at most [ ] {i.e., it has no side effects};
            procedure add (var s : String; c : char)
                modifies at most [s]
                {modifies only the string parameter s};
            function length (s: String) : integer
                modifies at most [ ] ;
            procedure append (var s1, s2, s3: string)
                modifies at most [s3]
                {only s3, the result of the operation, is modified};
        end StringSpec.

        Modularizing finite state machines

        • Statecharts do that
        • They have been incorporated in UML
        • They provide the notions of
          • superstate
          • state decomposition

        Sequential decomposition--chemical plant control example--

        Parallel decomposition