Formal Specifications Flashcards
What is a formal specification?
Part of a more general collection of techniques that are known as formal methods.
What are formal methods?
based on the mathematical representation and analysis of the software.
What do formal methods include?
Formal specification, specification analysis and proof, program verification.
Disadvantages of formal methods
Other techniques have been successful at increasing system quality. Do not reduce time to market. Not well suited to specifying and analyising user interfaces. Hard to scale up to large systems
Benefit of formal methods and where they are used?
Reducing the number of errors in systems and so main areas of applicability is critical systems : air traffil control, railway systems, spacecraft etc. Cost effective in these areas
name two specification techniques
algebraic approach- system is specified in terms of its operations and their relationships. However this is cumbersome when the object operations are not independent of the object state.
Model based approach - state model that is constructed using mathematical constructs. Operations are defined by modifications systems state. however it exposes the system state.
What is the use of formal spec?
involves investing more effort in the early phases of software development and this reduces errors as it forces a detailed analysis of requirements. Incompleteness and inconsistencies can be found and resolved so savings are made.
Why are sub system interface specifications important?
reduce the chance of misunderstanding between provider and user, The algebraic approach to formal specification is well suited to interface specification.
Structure of an algebraic spec
introduction- sort(type name). imports other specifications.
Description-informal descriptions of sort and its operations.
Signature-defines sytax of the interface to the abstract data type. (interface).
Axioms- defines semantics of the operations by defining axiom characterising behaviour.
Name some specification operations
constructor operations- create entites of the type being specified.
inspection operations- evaluate entites of the type being specified
what is AsmL(Abstract state machine language)
language for modelling and behaviour of digital systems. Can capture abstract stricture of discrete systems such as integrated circuits, software components, devices that combine hardware and software.
Why is an asml said to be abstract?
encodes only those aspects of the systems structure that affecet the behaviour being modelled. Helps us to reduce complex problems to manageable united.
What is the goal of asml?
use minimum amount of details that accurately reproduces or predicts the behavior
What is a sequence?
collection of elements of the same type but is ordered and can contain duplicate elements unlike sets.
whats quicksort?
discovered by tony hoare. Pick a pivot, partitiorn the items around the pivot so elements to left are smaller and bigger on right, Use recursion to sort both partitions.
