Information Technology Reference

In-Depth Information

Rippling can also be extended to support reasoning about logic programs

- and other situations where values are passed between conjoined relations

via shared existential variables, as opposed to being passed between nested

functions.

Relational

rippling

adapts

rippling

to

this

environment

[Bundy & Lombart, 1995].

3.3

Wave Annotations

Is the Concept of Wave-Rule a Formal or Informal One?
'Wave-rule'

can be defined formally. It is a rewrite rule containing wave annotation in which

the skeletons are preserved and the wave-front measure of the right-hand side

is less than that of the left-hand side. Informally, the skeleton consists of those

bits of the expression outside of wave-fronts or inside the wave-holes. The mea-

sure records the position of the wave-fronts in the skeleton. It decreases when

outwards directed wave-fronts move out or downwards wave-fronts move in. A

formal definition of skeleton and of the wave-front measure can be found in

[Basin & Walsh, 1996] and in chapter 4 of [Bundy

et al

, 2005].

Where Do the Wave Annotations in Wave-Rules and in Induction

Rules Come from?
Wave annotation can be inserted in expressions by a

family of difference unification algorithms invented by Basin and Walsh (see

[Basin & Walsh, 1993]). These algorithms are like unification but with the addi-

tional ability to hide non-matching structure in wave-fronts. Ground difference

matching can be used to insert wave annotation into induction rules and ground

difference unification for wave-rules. 'Ground' means that no instantiation of

variables occurs. 'Matching' means that wave-fronts are inserted only into the

induction conclusion and not the induction hypothesis. 'Unification' means that

wave-fronts are inserted into both sides of wave-rules. Note that the process of

inserting wave annotations can be entirely automated.

3.4

Performance

Has Rippling Been Used to Prove Any Hard Theorems?
Yes. Rippling

has been used successfully in the verification of the Gordon microprocessor and

the synthesis of a decision procedure and of the rippling tactic itself. It has also

been used outwith inductive proofs for the summing of series and the Lim+

theorem. A survey of some of these successes can be found in chapter 5 of

[Bundy

et al

, 2005].

Can Rippling Fail?
Yes, if there is no wave-rule available to move a wave-front.

In this case we apply critics to try to patch the partial proof. For inductive proofs,

for instance, these may: generalize the induction formula; revise the induction

rule; introduce a case split; or introduce and prove an intermediate lemma, ac-

cording to the precise circumstances of the breakdown. The fact that a failed

ripple provides so much information to focus the attempt to patch the proof is

Search WWH ::

Custom Search