* Lucid is an example of the "single - assignment statement" language. * Lucid is a formal system in which programs can be written and proofs of programs carried out. The proofs are easy to follow and straight- forward to construct because statements in a Lucid program are simply axioms from which the proof proceeds by conventional logical reason- ing, with the help of a few axioms and rules of inference for the special Lucid functions. * Lucid is an attempt to collapse the language in which assertions and proofs are expressed and the language in which the programs are written into a single formal system. * Lucid is a denotational language for the statements of a Lucid prog- ram can be interpreted as true mathematical assertions about the results and the effects of the program. For example, an assignment statement in Lucid can be considered as a statement of identity -- an equation. The order of statements is irrelevant. * Lucid can be used to express many types of reasoning -- partial correctness, termination, equivalence of programs ... * Similar formal mathematical systems, namely, recursive equations have existed which can be considered both as recipe and assertions about computing. These systems are discarded in favor for Lucid -- based on iteration as the recursive approach is considered to be too restrictive. Consequently, assignment and control flow of iteration is made mathematically more respectable. * Example -- a program to compute the integer square-root of a nat- ural number. In Prolog, root(N,X) :- s(0,1,N,X). s(I,J,N,I) :- J > N, !. s(I,J,N,X) :- add(I,1,K), add(I,I,L1), add(L1,3,L2), add(L2,J,L3), s(K,L3,N,X). where, add(I,J,K) :- K is I + J. In Lucid, N = first input first I = 0 first J = 1 next J = J + (2 * I) + 3 next I = I + 1 output = I as soon as J > N A sample proof for the above program in Lucid. * The variables and expressions in Lucid denote an infinite sequence (stream) of data objects. Statements are assertions about the history (world-line) of the variables. The ordinary data operations and relations and logical connectives work point-wise. Notion about non-strict functions, strict functions, constants, Lucid functions ... * Lucid as a potential language for specification. * Every variable in the Lucid program except "input" must be specified, and no variable may be specified twice. * Flavor of axioms about Lucid functions and rules of inference -- first(A + B) = first(A) + first(B) next(A + B) = next(A) + next(B) (X + Y) as soon as Q = (X as soon as Q) + (Y as soon as Q) first(first(X)) = first(X) next(first(X)) = first(X) first(X as soon as P) = (X as soon as P) next(X as soon as P) = (X as soon as P) first(P), P -> next(P) |= P eventually(Q), first(P), P & ~Q -> next(P) |= (P & Q) as soon as Q eventually(Q) |= (first(X) as soon as Q) = (first(X)) integer(K), K > next(K) |= eventually K < 0 * Lucid uses tense logic (a sort of modal logic) for reasoning about time. * Pitfalls in reasoning -- a. Axioms of data domain should account for the presence of undef- ined elements. b. The rules of inference of logical properties should accommodate an "undefined" truth value and the sequence nature of variables and expressions. * Examples of non-terminating statements, abortive computation, oper- ational semantics of variables, auxiliary variables, loop concate- nation, loop nesting, non-pointwise functions, recursive functions ... * Demand-driven dataflow as architectural implementation of Lucid. Account for lazy evaluation and provisions to avoid recomputation on same data values. * Lucid is nonprocedural for there is no room for side-effects in the language. * Many data types cannot be fitted into this denotational framework of Lucid, for example, arrays. * References -- 1. Ashcroft, E. A., and Wadge, W. W., Lucid, a nonprocedural lang- uage with iteration, CACM, 20, 7 (July 1977), 519-526. 2. Ashcroft, E. A., and Wadge, W. W., Lucid: A formal system for writing and proving programs, SIAM Journal of Computing, 5, 3 (September 1976), 336-354.