Mô tả:
Formal Specification
Formal Specification
Why?
• Precise standard to define and validate software
Why not?
• May be time consuming
• Methods not suitable for all applications
Formal Specification
Ben Potter, Jane Sinclair, David Till,
An Introduction to Formal Specification and Z
(Prentice Hall) 1991
Jonathan Jacky
The Way of Z
(Cambridge University Press) 1997
Mathematical Specification
Example of specification
B1, B2, ... Bk is a sequence of m x m matrices
1, 2, ... k is a sequence of m x m elementary matrices
B1-1 = 1
B2-1 = 21
Bk-1 = k ... 21
The numerical accuracy must be such that, for all k,
BkBk-1 - I <
Specification of Programming Languages
::= |
::= {}
::= . {} |
. {} E |
E
::= |
::= + | Pascal number syntax
Formal Specification Using Diagrams
unsigned integer
digit
unsigned number
unsigned integer
+
.
digit
unsigned integer
E
-
Two Rules
• Formal specification does not guarantee correctness
• Formal specification does not prescribe the implementation
Example: Z Specification Language
Informal: The function intrt(a) returns the largest integer
whose square is less than or equal to a.
Formal (Z):
intrt: N
N
a : N•
intrt(a) * intrt(a) < a < (intrt(a) + 1) * (intrt(a) + 1)
Example: Algorithm
1 + 3 + 5 + ... (2n - 1) = n2
Example: Program
int intrt (int a)
/* Calculate integer square root */
{
int i, term, sum;
term = 1; sum = 1;
for (i = 0; sum <= a; i++)
{
term = term + 2;
sum = sum + term;
}
return i;
}
Finite State Machine
A broadly used method of formal specification:
• Event driven systems (e.g., games)
• User interfaces
• Protocol specification
etc., etc., ...
Finite State Machine
Example:
Therapy control console
[informal description]
State Transition Diagram
Select field
Enter
Patients
Enter
Fields
Start
(ok)
Setup
Beam
on
Ready
Stop
(interlock)
Select patient
State Transition Table
Select Select
Enter
Patient Field
Patients
Fields Patients
Setup Patients Fields
Ready Patients Fields
Beam
on
ok
Start
Stop interlock
Fields
Setup
Ready
Beam
on
Setup
Ready Setup
Z Specification
STATE ::= patients | fields | setup | ready | beam_on
EVENT ::= select_patient | select_field | enter | start | stop
| ok | interlock
FSM == (STATE X EVENT)
STATE
no_change, transitions, control : FSM
Continued on next slide
Z Specification (continued)
control = no_change
transitions
no_change = { s : STATE; e : EVENT • (s, e)
transitions = { (patients, enter)
(fields, select_patient)
s}
fields,
patients, (fields, enter)
setup,
(setup, select_patient) patients, (setup, select_field)
(setup, ok)
ready,
fields,
(ready, select_patient) patients, (ready, select_field) fields,
(ready, start) beam_on, (ready, interlock) setup,
(beam_on, stop)
ready, (beam_on, interlock)
setup }
Schemas
Schema:
• The basic unit of formal specification.
• Describes admissible states and operations of a
system.
LibSys: An Example of Z
Library system:
• Stock of books
• Registered users.
• Each copy of a book has a unique identifier.
• Some books on loan; other books on shelves available
for loan.
• Maximum number of books that any user may have on
loan.
LibSys: Operations
• Issue a copy of a book to a reader.
• Reader return a book.
•
•
•
•
•
•
Add a copy to the stock.
Remove a copy from the stock.
Inquire which books are on loan to a reader.
Inquire which readers has a particular copy of a book.
Register a new reader.
Cancel a reader's registration.
LibSys
Level of Detail:
Assume given sets:
Copy, Book, Reader
Global constant:
maxloans
- Xem thêm -