Group: grammar
Group: natural language
Group: program proving
Group: requirement specification
Group: types of programming languages
Topic: abstraction as part of language
Topic: abstraction in programming
Topic: automated tests of specifications and designs
Topic: CADES structural modeling with holons
Topic: calculus of communicating processes
Topic: communicating sequential processes
Topic: curried functions
Topic: design documentation
Topic: design languages
Topic: functional programming
Topic: lambda calculus
Topic: limitations of formalism
Topic: logic programming
Topic: machine independent programming
Topic: model checker
Topic: models of parallel computation
Topic: Petri net
Topic: problems with logic programming
Topic: program proof via assertions
Topic: program proving is infeasible
Topic: programming as mathematics
Topic: programming language design
Topic: proving concurrent programs
Topic: reduction languages
Topic: referential transparency
Topic: safety critical systems
Topic: semantics by an abstract machine
Topic: setoriented languages
Topic: specification and design of distributed systems
Topic: specification is infeasible
Topic: state machine
Topic: Turing machine
Topic: type algebras, typed lambda calculus, and typecomplete languages
Topic: van Wijngaarden grammar
 
Summary
A formal method is using mathematics and logic to describe or analyze a system or program. If a system is logically sound, large classes of errors can not occur.
While attractive, formal methods come with a high cost. They need specialized talent and substantial time. A change may require a reanalysis of the system, making change impractical even when desired. Formal methods will not identify mistaken goals, requirements, and designs.
Formal methods are practical for errorprone domains such as state machines and concurrency. If a program clearly identifies concurrent and statecontrolled processes, automated analysis can check for problems.
Formal methods help define the semantics of a programming language. Without a formal semantics, further formal analysis is unfounded.
Formal descriptions can quickly become unwieldly. Tabular presentations help identify components with simple descriptions. (cbb 6/06)
Subtopic: reliability through formalism
Quote: more reliable elevator scheduler from formal methods than informal analysis; style also better; study using 20 teams [»sobeAE3_2002]
 Quote: readable, precise documentation is required; e.g., as input to tools [»hoffDM_2001]
 Quote: validated BOS's communication protocol with PROMELA and SPIN; identified an unsafe situation where only one door closed; intuitive chart of message sequence [»tretJ9_2001]
 Subtopic: formal method projects
Quote: Lucent uses virtual finitestate machines (VFSM) to separate the control behavior of a software module from its data manipulation; formal, executable, early error checking, 50% fewer defects, automatic documentation [»florAR1_1997]
 Quote: the VFSM validator exhaustively exercises a network of communicating VFSMs using the supertrace algorithm; found errors in three tested applications; widely used formal method [»florAR1_1997]
 Quote: ten commandments for successful projects using formal methods [»boweJP4_1995]
 Quote: use a small vocabulary for formal methods; easier to understand though longer, more abstract, little implementation bias; e.g., Hoare's CSP [»boweJP4_1995]
 Quote: use a formal methods team with a traditional design team; catches specification errors early [»boweJP4_1995]
 Quote: need a formal methods guru when using formal methods in a project [»boweJP4_1995]
 Quote: the length of a Z specification corresponds to the testing and development effort; useful for scheduling [»tretJ9_2001]
 Subtopic: requirements
Quote: use formal methods to verify a design instead of proving correctness; forces engineers to be precise about details; resolves differences of interpretation between implementers and testers [»tretJ9_2001]
 Quote: formal methods should improve reuse; they clearly state requirements with high component integrity without implementation bias [»boweJP4_1995]
 Subtopic: formal semantics
Quote: formal semantics for programming languages should play a fundamental role in software engineering [»parnDL10_1976]
 Quote: Esterel's formal semantics is based on constructive causality [»benvA1_2003]
 Quote: formal semantics enables compiletime optimization, analysis, and verification
 Quote: algorithm for evaluating an applicative expression relative to an environment; first formalization of expression evaluation
 Quote: operational semantics are good formal methods; intuitive, help implementers, simple, easy prototyping, easy integration [»degaP6_2001]
 Quote: a metacircular interpreter for expression evaluation defines each feature of the defined language via the corresponding feature of the defining language [»reynJC8_1972]
 Quote: formalization of XML Schema using tree grammars; named types and structural types; matching and validation [»simeJ1_2003]
 Quote: formalization of XML Schema used for XQuery and XPath specifications; one of the first
 Quote: XQuery standardization unanimously accepted pure named typing due to its simplification of formal semantics [»simeJ1_2003]
 QuoteRef: tennRD8_1976 ;;443 goes into Scott's formulations of semantic functions
 Subtopic: mixed formal and natural
Quote: BOS used formal Z specifications and natural language for detailed design; checked consistency, types, completeness; verified postconditions and invariants for highly critical subsystems [»tretJ9_2001]
 Quote: formal methods do not help with conceptual models and highlevel structuring; both require experience; formal specification gives a false feeling of confidence [»tretJ9_2001]
 Subtopic: state machine, automaton
Quote: an automaton is a black box that answers "yes" or "no" to arbitrary, finite sequences of symbols from a fixed, finite alphabet [»rabiMO4_1959]
 Quote: an automaton's operation is determined by finite, internal states; i.e., stable states of the machine at discrete time intervals; nothing else matters [»rabiMO4_1959]
 Quote: onetape, finite automaton are closed under backward tapes and complex products; forms a Boolean algebra of sets [»rabiMO4_1959]
 Quote: nondeterministic automaton equivalent to finite automaton; many choices at each move, with at least one winning combination; simpler description with fewer internal states [»rabiMO4_1959]
 Quote: finite automata do not support hierarchical design or concurrency; large, realtime systems are impossible to understand [»benvA9_1991]
 Quote: Lucent uses virtual finitestate machines (VFSM) to separate the control behavior of a software module from its data manipulation; formal, executable, early error checking, 50% fewer defects, automatic documentation [»florAR1_1997]
 Subtopic: testing
Quote: formal design specification allows test construction concurrently with coding; ready to test when coding finished [»tretJ9_2001]
 Quote: testers are effective reviewers of formal design specifications; they use the specifications to write their tests
 Subtopic: security language
Quote: secure DNS resolver in 10 lines of code; easier to understand than BIND's security policy [»jimT5_2000]
 Subtopic: combinators
Quote: use combinators to find the value of a financial contract; compositional, abstract valuation semantics [»joneSP9_2000]
 Quote: a financial contract has an acquisition date and an horizon or expiry date; (truncate t c) trims t's horizon to c [»joneSP9_2000]
 Quote: contracts in terms of observables; i.e., timevarying, objective measurements; e.g., temperature in LA [»joneSP9_2000]
 Quote: choose to acquire a financial contract (anytime u) or choose either contract (or) [»joneSP9_2000]
 Quote: use scoped combinators in Haskell for block and unblocking asynchronous interrupts; formal semantics
 Quote: the expression +/ in J is a tacit definition of summation; arguments are implicit; tacit definition is widely usable [»huiRKW8_1991]
 Quote: the tacit function 'f g h' is a fork that applies g to the results of f and h; e.g, 'a (+ * ) b' is '(a+b)*(ab)' [»huiRKW8_1991]
 Quote: J's primitives are one or two letters, e.g., $y for shape of y, #y for count of y, x,:y append itemized x to itemized y, f^:n y apply f n times to y [»huiRKW8_1991]
 Quote: APL has two function modifiers (reduction and cross product), but they can only combine with primitives [»backJ_1972]
 Subtopic: decision table
Quote: use tables to specify the postvalue of a variable for various combinations of prevalues [»parnDL12_1994]
 Subtopic: asynchronous
Quote: can interrupt a purelyfunctional computation at any point; allows asynchronous exceptions [»marlS6_2001]
 Subtopic: examples
Quote: used formal methods for BOS, the automated control system for Rotterdam's movable dam; highest safety integrity level; completed on time and within budget [»tretJ9_2001]
 Quote: validated BOS's communication protocol with PROMELA and SPIN; identified an unsafe situation where only one door closed; intuitive chart of message sequence [»tretJ9_2001]
 Quote: formal methods were used successfully; all of the software engineers found them useful [»tretJ9_2001]
 Quote: should have formalized the functional specification as well as the technical design; found problems, errors, ambiguities, and inconsistencies [»tretJ9_2001]
 Subtopic: history
Quote: to produce an utterance one has to refer back to general rules and forward to specific rules while reconstructing the rules from continuity, context, and exceptions [»misrVN_1966]
 Subtopic: problems with formal development
Quote: formal methods are less understandable than actual program text
 Quote: dealing with changed requirements is particularly painful for formal program development [»berrDM10_2002]
 Quote: requirements and proofs are inherently global; a changed requirement may require redoing most of the proofs; verification gets dropped [»berrDM10_2002]
 Quote: a simple error in Z can lead to a correct specification with a completely different meanings; e.g., forgetting a prime symbol ' to indicate the new state [»tretJ9_2001]

Related Topics
Group: grammar (8 topics, 181 quotes)
Group: natural language (16 topics, 539 quotes)
Group: program proving (10 topics, 311 quotes)
Group: requirement specification (11 topics, 307 quotes)
Group: types of programming languages (29 topics, 611 quotes)
Topic: abstraction as part of language (18 items)
Topic: abstraction in programming (67 items)
Topic: automated tests of specifications and designs (12 items)
Topic: CADES structural modeling with holons (24 items)
Topic: calculus of communicating processes (13 items)
Topic: communicating sequential processes (33 items)
Topic: curried functions (14 items)
Topic: design documentation (43 items)
Topic: design languages (12 items)
Topic: functional programming (45 items)
Topic: lambda calculus (16 items)
Topic: limitations of formalism (93 items)
Topic: logic programming (34 items)
Topic: machine independent programming (13 items)
Topic: model checker (49 items)
Topic: models of parallel computation (33 items)
Topic: Petri net (44 items)
Topic: problems with logic programming (10 items)
Topic: program proof via assertions (61 items)
Topic: program proving is infeasible (47 items)
Topic: programming as mathematics (27 items)
Topic: programming language design (53 items)
Topic: proving concurrent programs (37 items)
Topic: reduction languages (17 items)
Topic: referential transparency (26 items)
Topic: safety critical systems (32 items)
Topic: semantics by an abstract machine (38 items)
Topic: setoriented languages (20 items)
Topic: specification and design of distributed systems (14 items)
Topic: specification is infeasible (46 items)
Topic: state machine (67 items)
Topic: Turing machine (30 items)
Topic: type algebras, typed lambda calculus, and typecomplete languages (28 items)
Topic: van Wijngaarden grammar (9 items)
