Đăng ký Đăng nhập

Tài liệu Formal specification

.PDF
31
351
125

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 = 21 Bk-1 = k ... 21 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 -

Tài liệu liên quan