Page 191 - DCAP507_SYSTEM_SOFTWARE

Unit 12: Formal Systems and Programming Languages

A formal system comprises a formal language and a set of inference rules. The formal language Notes
includes primitive symbols that make up well formed formulas and the inference rules are
utilized to obtain expressions from other expressions inside the formal system. A formal system
may be formulated and considered for its intrinsic properties, or it may be proposed as a
depiction (i.e. a model) of external phenomena. In order to be truly functional in computer
science, we need our formal systems to be machine executable.

12.1 Use of Formal Systems in Programming Languages

Implementation concerned formally declared models can be measured as machine-independent
specifications of program behavior. They can proceed as "yard sticks" for the accuracy of program
conversions and optimizations.
Verification foundation of methods for analysis about program properties (e.g., equivalence)
and program specifications (program correctness). Language Design can bring to light vagueness
and unexpected subtleties in programming language builds.
Formal methods are system design methods that use thoroughly declared mathematical models
to construct software and hardware systems. In distinction to other design systems, formal
methods use mathematical evidence as a match to system testing so as to make sure correct
behavior. As systems become more complex, and security becomes a more significant issue, the
formal approach to system design provides another level of insurance.
Formal methods vary from other design systems via the use of formal verification systems, the
fundamental principles of the system must be confirmed accurate before they are accepted.
Traditional system design has utilized extensive testing to confirm behavior, but testing is
competent of only finite conclusions. Dijkstra and others have illustrated that tests can only
show the conditions where a system won't fail, but cannot say anything concerning the behavior
of the system outside of the testing situations. In distinction, once a theorem is confirmed true it
remains true.

Notes It is very significant to observe that formal verification does not prevent the
necessitate for testing. Formal verification cannot fix bad suppositions in the design, but
it can assist recognize errors in reasoning which would otherwise be left unconfirmed. In
numerous cases, engineers have reported locating flaws in systems once they reviewed
their designs formally

Approximately speaking, formal design can be viewed as a three step process, following the
sketch given here:
1. Formal Specification: Throughout the formal specification phase, the engineer thoroughly
defines a system by means of a modeling language. Modeling languages are fixed
grammars which permit users to model complex structures out of predefined types. This
process of formal specification is comparable to the process of translating a word problem
into algebraic notation. In numerous ways, this step of the formal design process is
comparable to the formal software engineering method developed by Rumbaugh, Booch
and others. At the minimum, both methods help engineers to evidently define their
problems, goals and solutions. However, formal modeling languages are more thoroughly
defined: in a formal grammar, there is a difference between WFFs (well-formed formulas)
and non-WFFs (syntactically incorrect statements). Yet at this stage, the difference between
WFF and non-WFF can help to state the design. Several engineers who have used formal
specifications say that the clearness that this stage generates is a advantage in itself.

LOVELY PROFESSIONAL UNIVERSITY 185