日本ソフトウェア科学会第 35 回大会 (2018 年度) 講演論文集

Transfinite Induction via Term Refinementin CafeOBJ
Kokichi Futatsugi

A transfinite induction method is formalized as a method for constructing proof scores in the CafeOBJ specification verification language system, and the eﬀectiveness of the method is demonstrated with a couple of
instructive examples.
Transfinite induction is induction in which a goal predicate can be assumed, as the induction hypotheses,
to hold for all values smaller than the goal value with respect to a well-founded order.
A property of interest on a specification (i.e. a goal property) is described as a Boolean ground termprp(c1,c2,..,cn) with fresh constants c1,c2,..,cn which corresponts to the parameters of the goal property.
A specification is formalized as a set of equations each of those can be interepreted as a left to right
reduction rule. The property proves to hold if the term prp(c1,c2,..,cn) is reduced to true.
Usually, term refinement of and induction on c1,c2,..,cn are necessary to show that prp(c1,c2,..,cn)
is reduced to true. The transfinite induction in CafeOBJ naturally combines the term refinement of andthe induction on c1,c2,..,cn, and has a potential to support a variety of inductions.

ification in this sense is theorem proving where a set

1 Introductionof axioms is the specification and theorems are the

CafeOBJ [2] is a state-of-the-art algebraic speci-

desirable properties.

fication language and is a member of the OBJ lan-

The theorem proving capability of CafeOBJ has

guage family [12] which also includes Maude [11].

been significantly enhanced with some achieve-

CafeOBJ is designed as an executable specification

ments including (1) formalization of induction andlanguage system which can be used as a specifica-

casesplit based on constructor-based specification

tion verification system [9] [4] [5] [6] [13].

calculus [8] and (2) specification/verification of

A CafeOBJ’s specification is a description ofmodels, and its verification is to show that the models has some desirable properties by deducing theproperties from the specification. Specification ver-transition systems with conditional transition rules[7] [13].

A proof score is a description in CafeOBJ ofa proof.

A specification in CafeOBJ is a setof equations, and CafeOBJ implements equational
CafeOBJ における項詳細化による超限帰納法
This is an unrefereed draft. The copyright belongs
to the Author.
二木厚吉, 産業技術総合研究所/国立情報学研究所/北陸
先端科学技術大学院大学, National Institute of Advanced Industial Science and Technology/National
Institute of Informatics/Japan Advanced Instituteof Science and Technology.

inference through reduction (i.e.

rewriting withthe equations by using them as left to right
rewrite/reduction rules). For a CafeOBJ’s specification (i.e. a specification module) M and a property p on M , expression M ⊨ p means that eachmodel of M satisfies p. If CafeOBJ returns truefor a reduction

reduce in M : p . (i.e. p reduces

its function (or meaning).

to true at module M ) then M ⊨ p is proved. A reduction that returns true is called eﬀective. A proof
score for M ⊨ p is a description of a set of eﬀective
reductions {’reduce in Mi : pi .’ | i = 1, 2, · · · , n}(including descriptions of modules that are necessary to execute the reductions) such that(M1 ⊨p1 and M2 ⊨p2 and · · · and Mn ⊨pn )implies M ⊨p
Proof scores can naturally describe several kindsof inductions including structural induction [1] [3],and quite a few cases are developed until now

01: --> --------------------------------------02: --> PNAT: Peano NATural numbers
03: --> --------------------------------------04: mod! PNAT {05: [Pnat]
06: op 0 : -> Pnat {constr} .
07: op s_ : Pnat -> Pnat {constr} .
08: }09: --> --------------------------------------10: --> PNAT with the addition _+_11: --> --------------------------------------12: mod! PNAT+ {13: pr(PNAT)
14: op _+_ : Pnat Pnat -> Pnat .
15: eq 0 + Y:Pnat = Y .
16: eq s X:Pnat + Y:Pnat = s(X + Y) .
17: }[5] [6] [13]. Transfinite induction seems to subsume

all of inductions used and could have a potential to

2. 2 Proof Score with Ordinary Induction

enhance eﬀectiveness and eﬃciency of proof scores.

The following CafeOBJ code (01:-40:)

is a

proof score for proving that the equation [assoc+]

2 An Explanatory Example(04:-06:) holds for any elements x, y, z of sort

Simple CafeOBJ specifications and proof scores

Pnat. That is, the binary operator _+_ satisfies theare presented, and several fundamental concepts
and techniques necessary for constructing proof
scores with transfinite induction are explained.

associative law.
ASSOC+ (10:-19:) is a module for writing theproof score.

It imports the base module PNAT+(12:) on which the property going to be proved
2. 1 Specification of _+_ on Peano Natural
Numbers(associativity in this case) applies.
Any property described with equations (likeThe following CafeOBJ module PNAT (04:-08:)

04:-06:) can be expressed with a Boolean ground

specifies Peano nutural numbers, and module PNAT+

term (a term without variables) with fresh con-(12:-17:) specifies a binary plus operator _+_ on

stants (as 14:+16-18:), and showing that thethe natural numbers.

Boolean ground term (assoc+ in this case) reducesLine number like 07: is for explanation and is notpart of CafeOBJ code, and CafeOBJ code starts

to true is suﬃcient for proving the property (seeProposition 3.2).

from the 4th column in each line.
Lines starting with -- or --> are comments (01:03:, 09:-11:)
Two constructor operators 0 and s_ are declared(06:-07:) and sort Pnat (05:) is defined as a setnz }| {of terms of the form s s · · · s 0 (n ∈ {0, 1, 2, · · ·}).
Pnat = {0, s 0, s s 0, s s s 0, · · ·}14: declares the rank (i.e. arity and co-arity) of
the binary plus operator _+_, and 15:-16: defines

01: --> =======================================
02: --> proof score for proving
03: --> associativity of _+_:
04: --> eq[assoc+]:
05: -->(X:Pnat + Y:Pnat) + Z:Pnat =06: -->X + (Y + Z) .
07: --> with the induction on X:Pnat
08: --> =======================================
09: --> module for declaring the goal of proof
10: mod ASSOC+ {11: -- the base module
12: pr(PNAT+)
13: -- Boolean ground term expressing the goal
14: pred assoc+ : .
15: -- fresh constants16: ops x y z : -> Pnat .
17: eq assoc+ =18:(((x + y) + z) = (x + (y + z))) .
19: }39: --> =======================================
40: --> =======================================

Comment expressed in 38:-40: indicates that

A CafeOBJ command ’red in ASSOC+ : assoc+ .’09:-37: is correct and eﬀective proof score fordoes not return true, and the proof does not suc-proving the equation 04:-06: in the comment

ceed. A common technique to proceed with the

01:-08: if 25: and 36: return true.

proof is case splitting. x is a fresh constant (i.e.
a constant never used in the context) of sort Pnat,
and, for another fresh constant x’, two equations

2. 3 Proof Score with Transfinite Induction’eq x = 0 .’ (23:) and ’eq x = s x’ .’ (32:) covers all

The following 01:-72: is another proof scorepossible cases. The specification of Pnat, 0, and s_

for proving the associativity equation [assoc+]

at 2. 1/05:-07: justifies this.

(11:-13:).

It uses transfinite induction, and’open ASSOC+ .’ (21:) opens module ASSOC+ and

47:-60: and 61:-70: is two diﬀerent pieces ofcreate a tentative module at which all sorts, opera-

code with a same function for executing reduc-tors, and equation of ASSOC+ are available. At thistions for the proof. That is, either of 17:-60: or

tentative module, after declaring ’eq x = 0 .’ (23:)

17:-46:+61:-70: is a correct and eﬀective proof

the reduction command ’red assoc+ .’ (25:) re-score for the equation [assoc+] (04:-06:).

turns true. This implies the proof is done for the

Module NAT< declared the fact 06: on the built-

case where ’eq x = 0 .’ (23:) holds, and 20:-26 is a

in greater-than predicate _<_ on built-in sort Nat

correct and eﬀective proof score for the inductionof built-in module NAT that is going to be used inbase case on x.

the proof score.

For the case where ’eq x = s x’ .’ (32:) holds, if

27:-39: defines the induction order _<io_ (32:)

the induction hypothesis on x’ is declared (34:),

on 3 tuples (X:Pnat Y:Pnat Z:Pnat) of three

the reduction command ’red assoc+ .’ (36:) re-parameters (variables) of the equation [assoc+]

turns true. This implies that the proof is done for(11:-13:). Note that the order _<io_ is irreflex-

the case where (32:) and (34:) hold, and 27:-37 isive and well-founded.

a correct and eﬀective proof score for the induction
step case on x.

40:-43: defines the induction hypothesis by aconditional equation with a condition composed of
the induction order _<io_. Note that this condi-

20: --> induction base on x
21: open ASSOC+ .
22: -- base case
23: eq x = 0 .
24: -- check the base
25: red assoc+ . --> succeed
26: close
27: --> induction step on x
28: open ASSOC+ .
29: -- fresh constant for refining x
30: op x’ : -> Pnat .
31: -- step case
32: eq x = s x’ .
33: -- induction hypothesis
34: eq (x’ + Y:Pnat) + Z:Pnat = x’ + (Y + Z) .
35: -- check the step
36: red assoc+ . --> succeed
37: close
38: --> QED

tional equation is eﬀective for any 3 tuple (X:Pnat
Y:Pnat Z:Pnat) that satisfies the condition ’(XY Z) <io (x y z)’, and constitutes induction hypotheses of transfinite induction.
Because _<io_ is well-founded, if assoc+ is reduces to true at module ASSOC+ind that includes
the induction hypothesis 40:-43:, then transfinite induction principle (Proposition 3.2)
guarantees that the goal equation 11:-13: holds
for any 3 tuple (X:Pnat Y:Pnat Z:Pnat).
01: --> ---------------------------------------

02: --> built-in NAT with FTBU on _<_03: --> --------------------------------------04: mod! NAT< {05: pr(NAT)
06: eq N1:Nat < NZ:NzNat + N1 = true .
07: }08: --> =======================================
09: --> proof score for proving
10: --> associativity of _+_:
11: --> eq[assoc+]:
12: -->(X:Pnat + Y:Pnat) + Z:Pnat =13: -->X + (Y + Z) .
14: --> with the transfinite induction
15: --> on 3 tuple (X:Pnat Y:Pnat Z:Pnat)
16: --> =======================================
17: -- module for proof with transfinite induction
18: mod ASSOC+ind {19: -- base module
20: pr(PNAT+)
21: -- goal Boolean ground term
22: pred assoc+ : .
23: -- fresh constants
24: ops x y z : -> Pnat .
25: eq assoc+ =26:(x + (y + z) = (x + y) + z) .
27: -- induction order
28: -- on 3 tuple (X:Pnat Y:Pnat Z:Pnat)
29: -- which is well founded order
30: [Pnat3tpl] op ___ : Pnat Pnat Pnat ->31:
Pnat3tpl {constr} .
32: pred _<io_ : Pnat3tpl Pnat3tpl .
33: pr(NAT<)
34: op sz : Pnat -> Nat .
35: eq sz(0) = 0 .
36: eq sz(s N:Pnat) = 1 + sz(N) .
37: eq (X1:Pnat Y:Pnat Z:Pnat) <io38:(X2:Pnat Y:Pnat Z:Pnat) =39:
sz(X1) < sz(X2) .
40: -- induction hypothesis
41: cq (X:Pnat + Y:Pnat) + Z:Pnat =42:
X + (Y + Z)
43:
if (X Y Z) <io (x y z) .
44: -- fresh constant for refinement
45: op x’ : -> Pnat
46: }’eq x = 0 .’ (52:) and ’eq x = s x’ .’ (57:) covers
all possible cases, and if both of ’red assoc+ .’ atule and include the goal equation. 65:-66: definesthat x is a proof rule for splitting the current goal(case) into two goals (cases) that include ’eq x = 0.’ (65:) or ’eq x = s x’ .’ (66:).
67: applies the proof rules x and rd successively
to the current goal. Applying x creates two subgoals (i.e. two tentative modules) by adding eachof the two equations to the current goal module respectively. Applying rd after x does reductions at
each of two sub-goals and check whether the goal
equation holds. If the goal equation holds, the goalis discharged. If all sub-goals of a goal is discharged,
the goal is dischaged, and the proof succeeds if theroot goal is discharged.
47: --> =======================================
48: --> proof score with open..close
49: -- case1 and case2 cover all possibilities
50: -- case1: eq x = 0 .
51: open ASSOC+ind .
52: eq x = 0 .
53: red assoc+ .
54: close
55: -- case2: eq x = s x’ .
56: open ASSOC+ind .
57: eq x = s x’ .
58: red assoc+ .
59: close
60: --> QED
61: --> =======================================
62: --> proof score with SpecCalc
63: select ASSOC+ind .
64: :goal{eq assoc+ = true .}65: :def x = :csp{eq x = 0 .
66:
eq x = s x’ .}67: :apply(x rd)
68: :show proof
69: :desc proof
70: --> QED
71: --> =======================================
72: --> =======================================

53: and 58: return true, then the proof succeeds.
The two reductions return true, and 17:-60: is’:apply(x rd)’ (67:) discharges all the createda correct and eﬀective proof score for [assoc+]

goals and the proof succeeds. 68: and 69: are(11:-13:).

commands for inspecting proofs. 73:-75: is out-

61:-70: execute the proof similarly as 48:-59:

put for 68:, and 78:-93: is output for 69:. 73:

by using the CafeOBJ’s specification calculus facil-shows the root goal, and 74:-75: shows two sub-ity. 63: select the base module where the proof

goals 1 and 2 created by the proof rule x. * after a

is executed. 64: declares that ’eq assoc+ = true

goal in 73:-75: shows that the goal is discharged.

.’ is the goal equation, and create a tentative goal

78:-93: describe the proof in more detail, andmodule called the root which import the base mod-shows direct correspondence between 47:-60: andv1 :Sort1 ,· · ·,vn :Sortn of specific sorts, and the61:-70: clearly.

property of interest is (∀v1 :Sort1 ,· · ·,∀vn :Sortn
73: root*
74: [x]1*
75: [x]2*
76:
78: ==> root*79:-- context module: #Goal-root80:-- targeted sentence:81:
eq assoc+ = true .
82: [x]1*83:-- context module: #Goal-1
84:-- assumption85:
eq [x]: x = 0 .
86:-- discharged sentence:87:
eq [RD]: assoc+ = true .
88: [x]2*
89:-- context module: #Goal-2
90:-- assumption
91:
eq [x]: x = s x’ .
92:-- discharged sentence:93:
eq [RD]: assoc+ = true .

3 Basics of Transfinite Induction via(prp(v1 ,· · ·,vn ))) (i.e. the parameters are universally quantified). Let c1 :Sort1 ,· · ·,cn :Sortn be n
fresh constants which correspond to the n parameters v1 :Sort1 ,· · ·,vn :Sortn . We get the following
proposition.
Proposition 3.2 [Theorm of constants](∀v1 :Sort1 ,· · ·,∀vn :Sortn (prp(v1 ,· · ·,vn ))) holds
if prp(c1 ,· · ·,cn ) reduces to true.
□
The original “Theorm of constants” in [10]states the definitional equivalence of the variables v1 :Sort1 ,· · ·,vn :Sortn and the fresh constants
c1 :Sort1 ,· · ·,cn :Sortn in defining algebraic models
and says nothing about reduction.

Term Refinement
This section presents basics of transfinite induction via term refinement in a modestly formal way.

3. 3 Casesplit with Equations
A module consists of a set St of sorts, a set Op
of operations, and a set Eq of equations declared

3. 1 Transfinite Inductionin the module. A model of the module is a system

Let Srt be a set of elements with a well foundedthat consists of the following two entities that sat-binary relation <io .

That is, there is no infi-

isfy all equations in Eq. (1) Sets which correspondnite sequence of elements e1 , e2 , e3 , · · · such thatto St. (2) Operations on the sets which correspond

ei+1 <io ei (i ∈ {1, 2, 3 · · ·}).

to Op.

The principle of transfinite induction is stated as

Let M be a module and p be a property on

follows.

M with universally quantified parameters, and let

Proposition 3.1 [Transfinite Induction]

M ⊨p mean that p holds for any model of M . As

Let p(X : Srt) be a predicate with a parameter of

explained in 3. 2, the property p can be assumed tosort Srt.

be expressed as a Boolean ground term. Let M ⊢r b(∀b ∈ Srt((∀a<io b(p(a))) implies p(b)))

mean that a Boolean ground term b reduces to true

implies (∀c ∈ Srt(p(c)))

at module M . The following restates Proposition□

3.2 by fixing the module of interest.
M ⊢r p implies M ⊨p
3. 2 Theorm of Constants(1)

Let e1 , · · · , en be equations such that at least one

In CafeOBJ, a property of interest on a moduleof them holds for any possible case. That is, theM is supposed to be described as a Boolean term

equations cover all the possibilities. Usually n is 2

composed of operators available at the module M .

or 3. Let M+ei be a module gotten by adding ei to

The Boolean term is expressed as prp(v1 ,· · ·,vn ),has n ∈ {0, 1, 2, · · ·} parameters (or variables)

M , then each model of M is a model of M+ej forsome j ∈ {1, 2, · · · , n}, and the following (2) statesthe principle of casesplit with equations.

except root can be considered to be a sequence of(M+e1 ⊨p and M+e2 ⊨p and · · · and M+en ⊨p)

non-zero natural numbers. Then the lexicograph-

implies M ⊨p (2)ical order can be defined over nodes except root;
root is assumed to be the first in the lexicographi-

3. 4 Term Refinement with Equations
A fresh constant is declared to be of some sort,and can be refined with equations which cover all
posibilites.
2. 1/05:-07: specifies sort Pnat and operators 0,
s_ as follows.
[Pnat]
op 0 : -> Pnat {constr} .
op s_ : Pnat -> Pnat {constr} .

Based on the above specification, a fresh constantcal order.
A symbol > is put to a node for indicating thenext node of a proof tree.
A proof tree is a tree structure of modules. Thatis, each node of the proof tree is a module for proving Mi ⊨pi for some Mi and pi , and the module
imports Mi and has equation ’eq pi = true .’ as
the targeted sentence. The node/module is calleda goal Mi ⊨pi . If Mi ⊢r pi the node/module/goal isdelcared as ’ op n : -> Pnat .’ can be refined into

discharged, and a symbol * is put to the node.

two possible cases with two equations ’eq n = 0 .’[Create the root Node] –and ’eq n = s n1 .’, where n1 is another fresh constant of sort Pnat (i.e. is delcared as ’ op n1 : ->Pnat .’).
n1 can be refined with similar two equations inturn, and n can be refined into a suﬃciently detailed term ’ s s ... s nm ’ of sort Pnat.

The following CafeOBJ code creates a modulewith a node root for proving M ⊨p.
select M .
:goal{eq p = true .}The current proof tree consists only of the noderoot. Put > to the node root (i.e. the goal M ⊨p),and make it the next goal.

3. 5 Specification Calculus
CafeOBJ code like 2. 3/63:-67: is a proof scorewith specification calculus (a SpecCalc proof score
for short). Specification calculus is going to be formalized as operations on proof trees caused by a
SpecCalc proof score. As a result, the SpecCalc
proof score is shown to present a semi-algorithm
for proving M ⊨p for a property p expressed as a
Boolean ground term on a module M .
For defining proof trees, nodes of a proof tree areexpressed as follows. root denotes the root nodeof a proof tree. n-1,n-2...n-k (k ∈ {1, 2, ...}) arechild nodes of node n, and n is the mother (or father) node of n-j (j ∈ {1, 2, ..., k}). A set T ofnodes is called a tree if n is an element of T thenthe mother of n is an element of T . A node in atree is called leaf if it has no child node.
A node root-n is abbreviated to n, and any node[Define Casesplit Equation Lists] –The following CafeOBJ code defines lists ofequations eqs1 , eqs2 , · · · , eqsl each list of which
eqsi = eqi1 eqi2 · · · eqimi (i ∈ {1, 2, · · · , l}) covers
all prossible cases, and can be used for casesplit.
Each of eqs1 , eqs2 , · · · , eqsl is called a caseslpit eqlist.
:def eqs1 = :csp{eq11 eq12 · · · eq1m1 }:def eqs2 = :csp{eq21 eq22 · · · eq2m2 }...
:def eqsl = :csp{eql1 eql2 · · · eqlml }[Apply sequence of :apply commands] –Let γ denote a sequence each element of which isa caseslpit eq-list eqsi or rd-, e.g.
γ = eqs1 rd- eqs2 rd- eqsm rd-.
Let t denote a proof tree and let n denote a nodein the proof tree, and let :apply(γ)@n[t] denotethe proof tree after applying :apply(γ1 ) to t at n.
The proof tree after applying a sequence of

:apply commands:apply(γ1 ) :apply(γ2 ) · · · :apply(γm )charged). If n is the next node, delete

to the current proof tree ct is defined as follows.
:apply(γm )@nm−1[:apply(γm−1 )@nm−2···[:apply(γ2 )@n1[:apply(γ1 )@n0 [ct]]· · ·]non-discharged leaf node (i.e. a leaf

> from n. Put > to the nearest next
node without *) in the lexicographic
order if such a node exits.
[If M m ⊢r pp does not hold] –Here n0 is the next node of the current proof tree

:apply(rd- γr )@n[t] =and ni is the next node of the proof tree after ap-:apply(γr )@n[t]The restatement of theorem of constants (1)plying :apply(γi )[Apply :apply command] –For a node n that does not have child nodes andand the principle of casesplit with equations(2) of 3. 3 justifies the following propostion.

is not discarged (i.e. to which * is not put) in a

Proposition 3.3 [SpecCalc]

proof tree t, :apply(γ)@n[t] is defined recursively

Let an initial proof tree consist only of the noderoot, which is a goal M ⊨p and is the next goal (i.e.

as follows.

to which > is put). If the application of a sequence[If γ is empty] –:apply(γ)@n[t] = t.
[If γ is not empty] –Let γ = r γr for r = eqs or r = rd-, and let
the node n be a goal M m⊨pp.

=:apply(γ1 ) :apply(γ2 ) · · · :apply(γm )(m ∈ {1, 2, · · ·})terminates and each node in the resultant proof tree
is discharged (i.e. to which * is put), then M ⊨p is[If r = eqs] –If eqsof :apply commands:

eq1 eq2 · · · eqm , then createm child nodes n-j of n for each j ∈{1, 2, · · · , m} such that the node n-j is aproved. □4 conclusion

goal M+eqj ⊨p. :apply(eqs γr )@n[t] is de-Transfinite induction has been formaized as afined as follows.
:apply(eqs γr )@n[t] =:apply(γr )@n-m[apply(γr )@n-(m−1)[· · ·[:apply(γr )@n-2[:apply(γr )@n-1[t]]· · ·]method for constructing proof scores in CafeOBJ.

If > is put to the node n (i.e. n is thenext node), then delete > from n and put
it to the node n-1, i.e. n-1 is the new next
node.
[If r = rd-] –[If M m ⊢r pp holds] –Put * to the node n to indicate thenode is discharged. For each node in
the current proof tree, put * to it if
each of its child nodes has * (i.e. is dis-

The formalized proof score method has the following characteristics.
• Induction hypotheses are directly declaredwith conditional equations (i.e.

conditional

reduction-rules), and a wide varaiety of induction hypotheses could be defined in an executable way.
• Casesplit with equations for searching all thepossible candidates can be applied uniformly
to the module in which induction hypotheses
are declared, and the principle of transfinite
induction stated at the proposition 3.2:(∀b ∈ Srt((∀a<io b(p(a))) implies p(b)))
implies (∀c ∈ Srt(p(c)))
is coded almost directly into the CafeOBJ codelike 2. 3/41:-43,63:-67:. 2. 3/63:-67: corresponds to the outer universal quantification∀b ∈ Srt, and 2. 3/41:-43 corresponds to theinner universal quantification ∀a<io b.
• Term refinement with equations is nicely combined with casesplit with equations and realizes
casesplit with term refinement. The casesplit with term refinement lies in the core of
specification calculus, and could make the fulluse of transfinite induction hypotheses defined

Maintaining Formal Specifications over Networks,First IEEE International Conference on Formal
Engineering Methods, ICFEM 1997, Hiroshima,
Japan, November 12-14, 1997, Proceedings, IEEE
Computer Society, 1997, pp. 170–182.
[10] Goguen, J.: Theorem Proving and Algebra, [Unpublished Book Draft].
[11] Maude: Web page, http://maude.cs.uiuc.edu/,
2018.
[12] The OBJ Family: Web page,
http://cseweb.ucsd.edu/~goguen/sys/obj, 2018.
[13] Kokichi Futatsugi (二 木 厚 吉): Introduction toSpecification Verification in CafeOBJ (モデルの記述と検証のためのプログラミング入門-CafeOBJ による仕様検証-), Saiensu-Sha (サイエンス社), 2017.

in conditional equations.

A Another Simple Example:
References[ 1 ] Burstall, R.:
Proving properties of programs by structural induction, Computer Journal,
Vol. 12(1)(1969), pp. 41–48.
[ 2 ] CafeOBJ: Web page, http://cafeobj.org/,
2018.
[ 3 ] Diaconescu, R.: Structural induction in institutions, Inf. Comput., Vol. 209, No. 9(2011),
pp. 1197–1222.
[ 4 ] Diaconescu, R. and Futatsugi, K.: Cafeobj
Report - The Language, Proof Techniques, andMethodologies for Object-Oriented Algebraic Specification, AMAST Series in Computing, Vol. 6,
World Scientific, 1998.
[ 5 ] Futatsugi, K.: Verifying Specifications with
Proof Scores in CafeOBJ, 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), 18-22 September 2006, Tokyo,
Japan, IEEE Computer Society, 2006, pp. 3–10.
[ 6 ] Futatsugi, K.:
Fostering Proof Scores in
CafeOBJ, Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China,
November 17-19, 2010. Proceedings, Dong, J. S. andZhu, H.(eds.), Lecture Notes in Computer Science,Vol. 6447, Springer, 2010, pp. 1–20.
[ 7 ] Futatsugi, K.: Generate & Check Method for
Verifying Transition Systems in CafeOBJ, Software,
Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement fromthe Chair of Programming and Software Engineering, Nicola, R. D. and Hennicker, R.(eds.), Lecture
Notes in Computer Science, Vol. 8950, Springer,
2015, pp. 171–192.
[ 8 ] Futatsugi, K., Gâinâ, D., and Ogata, K.: Principles of proof scores in CafeOBJ, Theor. Comput.
Sci., Vol. 464(2012), pp. 90–112.
[ 9 ] Futatsugi, K. and Nakagawa, A. T.: An
Overview of CAFE Specification Environment - An
Algebraic Approach for Creating, Verifying, andTotal Order _<_ on Pnat--> ----------------------------------------> PNAT with equality _=_--> --------------------------------------mod! PNAT={
pr(PNAT)
op _=_ : Pnat Pnat -> Bool {comm} .
eq ((s M:Pnat) = 0) = false .
eq (s M:Pnat = s N:Pnat) = (M = N) .
}--> ----------------------------------------> PNAT with greater predicate _<_--> --------------------------------------mod! PNAT<{
pr(PNAT=)
op _<_ : Pnat Pnat -> Bool .
eq 0 < s N:Pnat = true .
eq M:Pnat < 0 = false .
eq (s M:Pnat < s N:Pnat) = M < N .
}--> =======================================--> proof score for proving--> eq[ex<>=]:-->(M:Pnat < N:Pnat) xor-->(N < M) xor (M = N) xor-->((M < N) and (N < M) and (M = N))-->= true .
--> at module PNAT<--> with transfinite induction on 2 tuple--> (M:Pnat N:Pnat)--> via term refinement--> =======================================-- module for proof-- with transfinite induction
mod EX<>=ind {-- base modulepr(PNAT<)-- goal proposition
pred ex<>= : .
ops m n : -> Pnat . -- fresh constants
eq ex<>= =(m < n) xor (n < m) xor (m = n) xor((m < n) and (n < m) and (m = n)) .
-- induction order-- on 2 tuples of Pnat (M:Pnat N:Pnat)-- which is well founded order[Pnat2tpl] op __ : Pnat Pnat ->Pnat2tpl {constr} .
pred _<io_ : Pnat2tpl Pnat2tpl .
eq (M:Pnat N:Pnat) <io (s M s N) = true .
-- induction hypothesis-- for complete induction
cq (M:Pnat < N:Pnat) xor(N < M) xor (M = N) xor((M < N) and (N < M) and (M = N))= trueif (M N) <io (m n) .
-- fresh constants for refinement
ops m’ n’ : -> Pnat .
}--> =======================================-- specCalc proof score
select EX<>=ind .
:goal{eq ex<>= = true .}:def m = :csp{eq m = 0 . eq m = s m’ .}:def n = :csp{eq n = 0 . eq n = s n’ .}:apply(m n rd) -- succeed-:show proof:desc proof**> QED [ex<>=]--> =======================================--> =======================================#| -- comments start-- out put for :show proof
root*
[m]
1*
[n]
1-1*
[n]
1-2*
[m]
2*
[n]
2-1*
[n]
2-2*
-- out put for :disc proof==> root*-- context module: #Goal-root-- targeted sentence:

eq ex<>= = true .
1*-- context module: #Goal-1-- assumption
eq [m]: m = 0 .
-- targeted sentence:
eq ex<>= = true .
[n]
1-1*-- context module: #Goal-1-1-- assumptions
eq [m]: m = 0 .
eq [n]: n = 0 .
-- discharged sentence:eq [RD]: ex<>= = true .
[n]
1-2*-- context module: #Goal-1-2-- assumptions
eq [m]: m = 0 .
eq [n]: n = s n’ .
-- discharged sentence:eq [RD]: ex<>= = true .
[m]2*-- context module: #Goal-2-- assumption
eq [m]: m = s m’ .
-- targeted sentence:
eq ex<>= = true .
[n]
2-1*-- context module: #Goal-2-1-- assumptions
eq [m]: m = s m’ .
eq [n]: n = 0 .
-- discharged sentence:eq [RD]: ex<>= = true .
[n]
2-2*-- context module: #Goal-2-2-- assumptions
eq [m]: m = s m’ .
eq [n]: n = s n’ .
-- discharged sentence:eq [RD]: ex<>= = true .
[m]-- comments end |#