香港赛马会928282_com www.jonqp.tw Declarative View of Imperative Programs
By giving a declarative meaning to an imperative program, the verification of the imperative program is
switched from the imperative paradigm to the declarative or logic paradigm where one can take advantage
of, for example, referential transparency. Rather than ‘compiling’ an imperative program to a ‘lower level’
we ‘inverse compile’ the imperative program to the ‘higher’ declarative level. The declarative view of an
imperative program is a predicate associated with the imperative program such that if this predicate satisfies
the specification of the program then the imperative program is correct relative to the specification. In one
sense the associated predicate gives a declarative meaning to the imperative program.
“… and I do consider assignment statements and pointer variables to be among computer science’s ‘most valuable treasures’.”
D. Knuth 
In imperative programming, programs are implicitly state transformations. We want to abstract away from dealing with states and try to express programs within the “problem domain”, that is, we want to give a declarative meaning to imperative programs. If we want to sort a list, our program for doing this should deal with lists and use the properties of lists. Logic/Functional programming and also programming with assertions allow us to do this abstraction. Imperative programs may have functional and relational features - functions and procedures - but they also contain constructs which deal only with state transformation e.g. the assignment statement.
“Not only goto statements are being questioned: we hear complaints about floating-point calculations, global variables, semaphores, pointer variables, and even assignment statements.”
D. Knuth 
We are assuming a structured programming language without “goto” and the aim is to transform a structured program to a program without an assignment. We are not just complaining about the ‘assignment statement’, our aim is to show how it can be removed from programming. Without the assignment statement we gain the advantage of referential transparency (‘substitution of equals for equals’) which allows both for easier program verification and easier program construction. Also, by transforming a structured program to an ‘assignment-less’program we indicate a non-operational declarative meaning to the program.
2.Associating a Predicate with an Imperative Program.In the axiomatic semantics of Hoare/Dijkstra/Gries, a predicate pair gives the meaning of the imperative program and in this context a program is viewed as a predicate transformer, transforming a predicate to a predicate. For example, if we have a program, MOD, that calculates the ‘integer modulo function’ then the predicate pair
In the axiomatic semantics of Hoare/Dijkstra/Gries, a predicate pair gives the meaning of the imperative program and in this context a program is viewed as a predicate transformer, transforming a predicate to a predicate. For example, if we have a program, MOD, that calculates the ‘integer modulo function’ then the predicate pair
≥ 0 ∧ b > 0, Post(z,a,b): z = a mod b
2nd Irish Workshop on Formal Methods, 19981