Algebraic Example OBJ3.ppt

1、10/19/2000,cs599 - Formal Methods in Software Architecture,1,Algebraic Example OBJ3,Tarang Garg Srikumar Nagaraj,10/19/2000,cs599 - Formal Methods in Software Architecture,2,OBJ3 - Revision,“ OBJ3 is a wide spectrum first order functional language that is rigorously based upon equational logic.”Base

2、d on order sorted equational logic Provides notion of Subsort that rigorously supports multiple inheritance Exception handling and Overloading It is a theorem prover It gives powerful support for design and verification,10/19/2000,cs599 - Formal Methods in Software Architecture,3,Cruise Control,“ Th

3、e objects are identified by the Nouns in the specification and the interaction between the objects are identified by the Verbs.”Objects :Vehicle (not a required object for specs)brakeaccelerator pedal CC(cruise control) button On /OffCC button Set/Accelerator CC button Resume/Decelerator,10/19/2000,

4、cs599 - Formal Methods in Software Architecture,4,Cruise Control,Assumptions: * 1. If cruise-speed = 0 then the car is not cruisingand if cruise-speed 0 then the car is cruising. 2. cruise_state represents the button. 3. Max. allowed speed is 140 mph. 4. The car does not take any time to change spee

5、ds. * th CAR-STATE is sort INT . protecting INT .protecting TRUTH-VALUE . op init1_ : INT INT .op init2_ : TRUTH-VALUE TRUTH-VALUE .vars curr_speed cruise_speed last_cruise_speed : INT .var cruise_state : TRUTH-VALUE . eq init1 curr_speed = 0 .eq init1 cruise_speed = 0 . eq init1 last_cruise_speed =

6、 0 .eq init2 cruise_state = false . endth,10/19/2000,cs599 - Formal Methods in Software Architecture,5,Cruise Control,obj CC-ON-OFFV-CAR-STATE : CAR-STATE .protecting TRUTH-VALUE .op cruise-press_ : TRUTH-VALUE TRUTH-VALUE .var I : TRUTH-VALUE .cq cruise-press (cruise_state) = (I = false) * This che

7、cks for the cruise control button if it is ONif cruise-state = true .eq cruise-state = I .cq cruise-press (cruise-state) = (I = false) and (last-cruise-speed = 0) * This checks for the cruise control button if it is OFFif cruise-state = false . endo,10/19/2000,cs599 - Formal Methods in Software Arch

8、itecture,6,Cruise Control,obj CC-SET-ACCELERATEV-CAR-STATE : CAR-STATE .protecting INT .protecting TRUTH-VALUE .op button-press_ _ _ : INT INT TRUTH-VALUE INT INT INT .op button-press_ _ : INT TRUTH-VALUE INT INT .op time_ : INT INT .vars X Y : INT .cq button-press (cruise-speed , curr-speed , cruis

9、e-state) = (cruise-speed = curr-speed) and (last-cruise-speed = cruise-speed) if (cruise-state = true) and (curr-speed 30)and (curr-speed 30) and (cruise_speed 90) .eq time X = Y . endo* Assumption: Time is a function which takes time in seconds(X) for which SET is pressed & gives * the speed factor

10、(Y) to add to cruise-speed.,10/19/2000,cs599 - Formal Methods in Software Architecture,7,Cruise Control,obj CC-RESUME-DECELERATEV-CAR-STATE : CAR-STATE .protecting INT .protecting TRUTH-VALUE .op button-press_ _ _ _ : INT INT INT TRUTH-VALUE INT INT op button-press_ _ : INT TRUTH-VALUE INT INT . op

11、time_ : INT INT .vars X Y : INT .cq button-press (cruise-speed , curr-speed , last-cruise-speed, cruise-state) = (cruise-speed = last-cruise-speed) if (cruise-state = true) and (curr-speed 30) and (curr-speed 90)and (cruise-speed = 0) and (last-cruise-speed =/= 0) .cq button-press (cruise-speed , cr

12、uise-state) = (cruise-speed = cruise-speed Y ) and (last-cruise-speed = cruise-speed)if (cruise-state = true) and (cruise-speed =/= 0) .eq time X = Y . endo *Assumption: Time is a function which takes time in seconds(X) for which RESUME is * pressed and gives the speed factor(Y) to subtract to cruis

13、e-speed.,10/19/2000,cs599 - Formal Methods in Software Architecture,8,Cruise Control,obj ACCELERATOR-PEDALV-CAR-STATE : CAR-STATE . protecting INT .op pedal-press_ _ : INT INT INT .op time_ : INT INT .op uphill _ _ : INT INT INT .vars X Y : INT .cq pedal-press (curr-speed , cruise-speed) = (curr-spe

14、ed = curr-speed + Y)if (cruise-speed = 0) and (curr-speed 140) .eq time X = Y . cq uphill (curr-speed, cruise-speed) = ( curr-speed = curr-speed + Z) and (cruise-speed = curr-speed)if (cruise-speed =/= 0) and (current-speed cruise-speed) . endo * Assumption: Time is an operation which takes time in

15、seconds(X) for which pedal is * pressed and returns the factor(Y) by which the speed is to be increased. * Z is a factor which gives the drop in the speed when the car goes uphill,10/19/2000,cs599 - Formal Methods in Software Architecture,9,Cruise Control,obj BRAKE-PEDALV-CAR-STATE : CAR-STATE .prot

16、ecting INT .op pedal-press_ _ : INT INT INT .op pedal-press_ : INT INT INT INT .op time_ : INT INT .op downhill _ _ : INT INT INT .vars X Y : INT .cq pedal-press (curr-speed , cruise-speed) = (curr-speed = curr-speed X)if (cruise-speed = 0) and (curr-speed 0) .cq pedal-press (cruise-speed) = (cruise

17、-speed = 0) and (last-cruise-speed = 0)if (cruise-speed =/= 0) .eq time X = Y . eq downhill (curr-speed, cruise-speed) = ( curr-speed = curr-speed - Z) and (cruise-speed = curr-speed)if (cruise-speed =/= 0) and (current-speed cruise-speed) . endo * Assumption: Time is an operation which takes time f

18、or which the pedal is pressed and * returns the factor by which the speed is decreased. * Z is the factor which gives the increase in the speed when the car goes downhill,10/19/2000,cs599 - Formal Methods in Software Architecture,10,Gas Station,Assumptions * 1. When the customer goes to the cashier

19、& pays cash, the cashier allots a pump no. & a password to the customer. 2. Pump has one nozzle and three buttons for premium, plus & regular. 3. type-of-gas has integer values viz. plus 1 $1.90 per gallonregular 2 $ 1.80 per gallonpremium 3 $ 2.00 per gallon * Objects:pumpnozzlecustomercashiercar (

20、unnecessary)Gas tank car tank (unnecessary)sensor meter on the pump (unnecessary),10/19/2000,cs599 - Formal Methods in Software Architecture,11,Gas Station,th PASSWORD is sort INT .protecting INT .protecting TRUTH-VALUE .op init1_ : TRUTH-VALUE TRUTH-VALUE .op init2_ : INT INT .var enable-pump : TRU

21、TH-VALUE .vars pump-password-value customer-password-value : INT .eq init1 enable-pump = false .eq init2 pump-password-value = 0 .eq init2 customer-password-value = 0 . endth th TANK-STATES is sort INT .protecting INT .op init1_ : INT INT .vars amount-gas-car-tank amount-gas-station-tank : INT .eq i

22、nit1 amount-gas-car-tank = 0 .eq init1 amount-gas-station-tank threshold . endth * Assumption: threshold is some integer value which is pre-defined for the tank. * Initially we are assuming that the gas in the GAS STATION TANK is greater than threshold.,10/19/2000,cs599 - Formal Methods in Software

23、Architecture,12,Gas Station,th GAS-STATE is sort INT .protecting INT .protecting FLOAT .protecting TRUTH-VALUE .op init1_ : TRUTH-VALUE TRUTH-VALUE .op init2_ : INT INT .vars nozzle-up lever-press : TRUTH-VALUE .var type-of-gas amount-gas-dispensed : INT .var amount-charged : FLOAT .eq init1 nozzle-

24、up = false .eq init1 lever-press = false .eq init2 type-of-gas = 0 . eq init2 amount-gas-dispensed = 0 .eq init2 amount-charged = 0 . endth * the gas is not selected right now,10/19/2000,cs599 - Formal Methods in Software Architecture,13,Gas Station,th CASH-STATE is sort INT .protecting INT .protect

25、ing TRUTH-VALUE .op init1_ : TRUTH-VALUE TRUTH-VALUE .op init2_ : INT INT .vars cash-given-by-customer pump-number : INT .var receipt : TRUTH-VALUE .eq init1 receipt = false .eq init2 cash-given-by-customer = 0 .eq init2 cash-received-as-change = 0 .eq init2 pump-number = 0 . endth * initially there

26、 is no cash transaction,10/19/2000,cs599 - Formal Methods in Software Architecture,14,Gas Station,obj PUMPV-PASSWORD : PASSWORD , V-GAS-STATE : GAS-STATE .protecting INT .protecting FLOAT .protecting TRUTH-VALUE .op give-receipt_ _ : INT INT FLOAT .op choose-gas-type_ _ : TRUTH-VALUE TRUTH-VALUE INT

27、 .op calculate-rate_ : FLOAT FLOAT .var X : FLOAT .var Y : INT .cq give-receipt (amount-gas-dispensed , type-of-gas) = (amount-charged = (amount-gas-dispensed * X) if (type-of-gas =/= 0) and (amount-gas-dispensed =/= 0) .cq choose-gas-type (nozzle-up , lever-press) = (type-of-gas = Y)if (nozzle-up =

28、 true) and (lever-press = false) .eq calculate-rate (type-of-gas) = (X = 1.80) if (type-of-gas = 2).eq calculate-rate (type-of-gas) = (X = 1.90) if (type-of-gas = 1).eq calculate-rate (type-of-gas) = (X = 2.00) if (type-of-gas = 3). endo * Y is 1 when type of gas chosen is PLUS * Y is 2 when type of

29、 gas chosen is REGULAR * Y is 3 when type of gas chosen is PREMIUM,10/19/2000,cs599 - Formal Methods in Software Architecture,15,Gas Station,obj NOZZLEV-GAS-STATE : GAS-STATE .protecting INT .protecting TRUTH-VALUE .op dispense-gas_ _ _ : TRUTH-VALUE TRUTH-VALUE INT INT INT .op lift-nozzle_ _ : INT

30、INT TRUTH-VALUE .op keep-nozzle-back_ _ : TRUTH-VALUE TRUTH-VALUE INT TRUTH-VALUE .op lever-press_ _ : TRUTH-VALUE INT TRUTH-VALUE .op cal_ : INT INT .vars X Y : INT .cq dispense-gas (nozzle-up , lever-press , type-of-gas) = (amount-gas-car-tank = amount-gas-car-tank + Y) and(amount-gas-station-tank

31、 = amount-gas-station-tank Y) if (nozzle-up = true) and (lever-press = true) and (type-of-gas =/= 0) .cq lift-nozzle (pump-password-value , customer-password-value) =(nozzle-up = true) if (pump-password-value = customer-password-value) .cq keep-nozzle-back (nozzle-up , lever-press) = (customer-passw

32、ord-value = 0) and (nozzle-up = false)if (nozzle-up = true) and (lever-press = false) .cq lever-press (nozzle-up , type-of-gas) = (lever-press = true)if (nozzle-up = true) and (type-of gas =/= 0) .eq cal X = Y . endo * cal is a function which calculates the amount of gas dispensed taking the time fo

33、r which the nozzle is * pressed. The customer comes to the pump assigned and enters the password for enabling the pump,16,Gas Station,obj CUSTOMERV-CASH-STATE : CASH-STATE .protecting INT .protecting FLOAT .protecting TRUTH-VALUE .op gives-cash_ _ : INT INT INT .op receives-balance_ _ _ : TRUTH-VALU

34、E FLOAT FLOAT TRUTH-VALUE FLOAT .op receives-receipt_ _ : TRUTH-VALUE INT TRUTH-VALUE .var cash : FLOAT .cq gives-cash (customer-password-value , cash-given-by-customer) = (cash-given-by-customer = cash)if (customer-password-value = 0) and (cash-given-by-customer = 0) .cq receives-balance (nozzle-up

35、, cash-given-by-customer, amount-charged) = (enable-pump = false) and (cash-received-as-change = cash-given-by-customer amount-charged) and(customer-password-value = 0)if (nozzle-up = false) and (cash-given-by-customer =/= 0) and (cash-given-by-customer amount-charged) .cq receives-receipt (nozzle ,

36、 amount-gas-dispensed) = (receipt = true)if (nozzle-up = false) and (amount-gas-dispensed =/= 0) and (amount-charged =/= 0). endo * cash is the amount of cash given by the customer to cashier for the gas.,10/19/2000,cs599 - Formal Methods in Software Architecture,17,Gas Station,obj CASHIERV-CASH-STA

37、TE : CASH-STATE .protecting INT .protecting FLOAT .protecting TRUTH-VALUE .op receives-cash_ : INT FLOAT INT INT TRUTH-VALUE .op gives-change_ _ _: TRUTH-VALUE INT FLOAT TRUTH-VALUE INT INT INT .var cash : FLOAT .var pval : INT .cq receives-cash (cash-given-by-customer) = (cash-given-by-customer = c

38、ash ) and (pump-password-value = pval) and (customer-password-value = pval)and (enable-pump = true)if (cash-given-by-customer = 0) .cq gives-change (nozzle, amount-gas-dispensed, amount-charged) = (enable-pump = false) and (pump-password-value = 0 )and (customer-password-value = 0) and (amount-gas-d

39、ispensed = 0)if (nozzle = false) and (amount-gas-dispensed =/= 0) and (amount-charged =/=0) . endo * pval is a randomly generated number which is given as password to each customer. It * never repeats.,10/19/2000,cs599 - Formal Methods in Software Architecture,18,Gas Station,obj GAS-TANK-PUMPV-TANK-

40、STATES : TANK-STATES .protected INT .op supply-gas-to-pump_ : INT INT .var X : INT .cq supply-gas-to-pump (amount-gas-station-tank) = (amount-gas-station-tank = amount-gas-station-tank + X)if (amount-gas-station-tank threshold) . endo * Assumption: threshold is the pre-defined value for the tank. *

41、X is the value of gas required to make the gas station tank full, it depends on the amount of gas already present in the tank. obj SENSORV-GAS-STATES : GAS-STATES .protecting INT .protecting TRUTH-VALUE.var max-tank-capacity : INT.op sense-gas-full_ : INT TRUTH-VALUE .cq sense-gas-full (amount-gas-c

42、ar-tank) = (lever-press = false) if (amount-gas-car-tank = max-tank-capacity) . endo * max-tank-capacity is the maximum capacity of the gas car tank (dependent on the type of car), i.e. car specific.,10/19/2000,cs599 - Formal Methods in Software Architecture,19,Inferences,It goes in a lot of details

43、 like the sorts and the subsorts It is good in a place where accuracy is the prime issue and the details are the requirement while modeling the system. Where lot of calculations are required. It has got an Exceptional handling feature which can be very efficiently used to handle exceptions. Very nea

44、r to the implementation languages specially OOPS like C+ and Java, etc. Would be liked by the coder.(directly lead to the code) Not very good for state based problems, difficult to represent states.,10/19/2000,cs599 - Formal Methods in Software Architecture,20,Our Approach,Dependent on OOPs Chose th

45、e Objects (nouns of the specs) Then chose the theories Chose the operations for each object (interactions) Then declared the objects with their operations. Extensively used function overloading. Made assumptions where ever required.,10/19/2000,cs599 - Formal Methods in Software Architecture,21,Diffi

46、culties Faced,There is no form of diagrams here which explains the details of the problem. If the spec is very complicated then it is very difficult to understand. It can be used in the intermediate stage of design and implementation, but not for design, if the specs are very complicated. Did not understand the use of views. Did not use any Exception handling feature of OBJ3.,