"The doors must not be open on a given floor unless the elevator is stopped at that floor." 

这句话往往就是作为规范写入我们的文档中的。而如果采用 Logic 的形式，那么就可能是类似于以下的样子：

e: an elevator, f: a floor.
Position(e, f) means e is at the f floor
Stopped(e) means e is stopped
Door_Open(e, f) means e’s door is open on 
the floor f   
ALL(e: elevator, f: floor:: (Door_Open(e, f) =>
(Position(e, f) & Stopped(e)) ))

  DEFINITION airline_environment

  INHERIT system  --  defines software_system, proposed.

--  controls

INHERIT user  --  defines User_class, uses

INHERIT business  --  defines vendor, customer, sells

IMPORT Subtype FROM type

CONCEPT airline_reservation_system: software_system

  WHERE proposed (airline_reservation_system),

        --We are going to build an airline reservation

-- system

     Controls (airline_reservation_system, reservation)

       --The system will help travel agents sell tickets by

       --managing reservations.

CONCEPT travel_agent: User_class

  WHERE ALL(ta: travel_agent

::uses(ta, airline_reservation_system)),

        --Travel agents use the airline reservation system.

        --We are only concerned with the travel agents using

        --our system.

Subtype(travel_agent, vendor),

--A travel agent is a sales person.

ALL(t : ticket :: SOME (ta: travel_agent

:: sells(ta, t) )),

    ALL(r: reservation :: SOME (ta: travel_agent

      :: supplies(ta, t) ))

--Travel agents are the only sources for tickets

--and reservations.

CONCEPT ticket: type

   WHERE Subtype(ticket, product),

      ALL (t: trip :: Needed_for(ticket, t))

--A ticket is needed for every trip.

CONCEPT trip : type

   WHERE Subtype (trip, activity),

      ALL(t: trip :: Needed_for (flight, t))

--A flight is needed for every trip.

CONCEPT passenger : type

WHERE Subtype (passenger ,custom),

      ALL (p: passenger :: SOME(t: trip :: wants(p, t))),

ALL (p: passenger :: SOME(t: ticket :: buys(p, t)))

CONCEPT airline : type

WHERE Subtype(airline, supplier),

      ALL(f: flight :: SOME(a: airline :: supplies(a, f)))

        --Every flight is associated with an airline.

        --We are only concerned with commercial flights.

CONCEPT flight :type

WHERE Subtype(flight, activity)

CONCEPT reservation : type

WHERE ALL (t: trip :: SOME(r: reservation

 :: Neded_for (r, t)))

END

经过精化 (Refine) 之后的一个 Environment Model

DEFINITION flight_view
INHERIT time
INHERIT location
IMPORT Subtype FROM type
IMPORT One_to_one FROM function (flight, flight_id)

CONCEPT flight: type
    - -The passenger will choose a flight based on origin,
    - -destination, departure, arrival, and price.
WHERE Subtype (flight, activity)

  CONCEPT origin (f: flight) VALUE (a: airport)
CONCEPT destination (f: flight) VALUE (a: airport)
CONCEPT departure (f: flight) VALUE (t: time_of_day)
CONCEPT arrival (f: flight) VALUE (t: time_of_day)
CONCEPT price (f: flight) VALUE (m: money)
CONCEPT id (f: flight) VALUE (i: flight_id)
   - - The flight id is used by the passenger to find
   - - the flight.
   WHERE One_to_one (id)   - - The id uniquely identifies
                           - - a flight.

CONCEPT airport: type
   WHERE Subtype (airport, location)

CONCEPT flight_id: type

CONCEPT airline: type 
   WHERE Subtype (airline, supplier),
      ALL (f: flight :: SOME (a: airline :: supplies (a, f) ) )
        - - Every flight is associated with an airline.
        - -We are only concerned with commercial flights.
END

第三个概念是 Functional Spec 中的 FUNCTION、MACHINE、TYPE。这些东西用于定义系统中的各个模块。FUNCTION 表示变量域与值域存在的映射关系；MACHINE 表示一个状态机；TYPE 表示一种可有多个实例的类型。它们的定义语法如下：

FUNCTION function_name
--inherit , import , export section
--message definitions
--concept definitions
END

MACHINE machine_name
--inherit , import , export section
--state model definition
--message definitions
--concept definitions
END

TYPE type_name
--inherit , import , export section
--instance model definition
--message definitions
--concept definitions
END

以下是一个 FUNCTION 的例子：

FUNCTION square_root {precision:real SUCH THAT precision > 0.0}
    MESSAGE(x:real) - - anonymous message
        WHEN x >= 0.0 - -  precondition
            REPLY(y:real) - - return value
            WHERE Y >= 0.0 AND                         approximate(y*y,x)
            OTHERWISE REPLY EXCEPTION
                imaginary_square_root
CONCEPT approximate(r1,r2:real)
    - - true if r1 is a sufficiently accurate approximation of r2, based on the value of the precision specified by the user
    VALUE(b: boolean )
        WHERE
            babs(r1-r2)<=abs(r2*precision)
END

可以看到，通过这种方式精确定义了一个功能模块的“黑箱”行为。

第四个概念 Stimulus-Response Diagram。这个 Diagram 用于显示以上三种 Spec Language 的输入、输出流。对于上面的实例 FUNCTION ，有下面的图：

限于篇幅以及个人的理解，目前就写这些。给出一个 Case Study ，供有兴趣的朋友学习。