Formal Method Lecture
Specification languages are formal languages used to specify the behaviour or
properties of a system, software, or hardware. They are used to describe the
requirements of a system in a precise and unambiguous way, so that developers can
understand them and implement the system correctly.
Specification languages can be used to specify various aspects of a system, such as
its functionality, performance, safety, security, and reliability. They can be used to
specify requirements at different levels of abstraction, from high-level functional
requirements to low-level implementation details.
Some examples of specification languages include Z, VDM, B, Alloy, and TLA+. These
languages are often used in formal methods, which are mathematical techniques
used to verify the correctness of a system's behaviour or properties.
Specification languages play an important role in software engineering, as they help
ensure that software systems are developed to meet their intended requirements
and behave correctly in all circumstances.
Program refinement and derivation are two related concepts in software engineering
that involve systematically transforming a high-level specification of a program into a
lower-level implementation.
Program refinement involves the stepwise transformation of an abstract specification
into a more concrete and detailed one, until it can be directly translated into code.
Refinement is typically done in a series of steps, with each step refining the
specification by adding more details and removing ambiguities. At each step, the
refined specification should be equivalent to the original specification, but more
detailed and precise.
Program derivation, on the other hand, involves the systematic generation of a
program from its specification, using a set of transformation rules and inference
rules. Derivation is often done using formal methods, which are mathematical
techniques used to reason about the correctness of programs. The goal of program
derivation is to ensure that the generated program correctly implements the
intended behaviour specified by the original specification.
Both program refinement and derivation are used to ensure that software is
developed correctly and meets its intended requirements. They are often used in
safety-critical and high-assurance systems, where the correctness of the software is
of utmost importance.
Formal verification is a method of ensuring that a system or software meets its
intended requirements or specifications using mathematical techniques. It involves
the use of formal methods, which are mathematical tools and techniques used to
specify, model, and reason about software systems.
In formal verification, the software or system is first specified using a formal
specification language, which provides a precise and unambiguous description of the
system's behaviour. The specification is then subjected to various formal verification
techniques, such as model checking, theorem proving, or abstract interpretation, to
verify that the system satisfies its requirements.
Formal verification can help detect and eliminate errors or bugs in a system or
software before it is deployed, which can save time and money in the long run. It is
particularly useful in safety-critical and high-assurance systems, such as aircraft
control systems, medical devices, and nuclear power plants, where even a small error
can have catastrophic consequences.
However, formal verification can be time-consuming and requires specialized
expertise, which can make it expensive and impractical for certain types of software.
As a result, it is often used in combination with other testing and verification
methods to ensure the correctness and reliability of software systems.
Logical inference is the process of deriving new knowledge or conclusions from
existing knowledge or premises using logical reasoning. It involves applying rules of
logic to a set of premises or assumptions to arrive at a logical conclusion or
inference.
In logical inference, the premises or assumptions are usually expressed using a
formal language, such as propositional logic or predicate logic, which provides a
precise and unambiguous representation of the knowledge or information being
used. The rules of logic are then applied to these premises to determine what
conclusions can be logically inferred from them.
Logical inference is used in many fields, including mathematics, computer science,
philosophy, and artificial intelligence. In mathematics, logical inference is used to
prove theorems and derive new mathematical results. In computer science, logical
inference is used in formal verification to verify the correctness of software systems.
In philosophy, logical inference is used to analyse arguments and determine their
validity.
Some common types of logical inference include deductive reasoning, inductive
reasoning, and adductive reasoning. Deductive reasoning involves deriving a
conclusion that is necessarily true given the premises, while inductive reasoning
involves deriving a conclusion that is likely to be true based on the available
evidence. Adductive reasoning involves deriving a plausible explanation or
hypothesis for a set of observations or data.
