Path: csiph.com!eternal-september.org!feeder.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Mike Amling <mamling@chaff.us>
Newsgroups: comp.lang.java.programmer
Subject: Program proof
Date: Tue, 5 Jul 2016 11:23:26 -0500
Organization: A noiseless patient Spider
Lines: 53
Message-ID: <nlgmte$3o3$1@dont-email.me>
References: <drj6nb1mja17fads03ucr3v7mi2fcn2d36@4ax.com> <slrnnn6op7.456.avl@login.logic.tuwien.ac.at> <ads6nbhnkttcdfudcnemafu5gdeul2uq45@4ax.com> <86lh1o4eku.fsf@kwarg.de> <System.class-20160629205023@ram.dialup.fu-berlin.de> <nl36hi$704$1@dont-email.me> <11952827-9dd1-48e7-b835-722a38023ce5@googlegroups.com> <nl39pj$o53$1@dont-email.me> <00835840-56aa-4ba2-b496-e364a62a38e8@googlegroups.com> <nl3d72$4qn$1@dont-email.me> <nl3o2f$b28$1@dont-email.me> <nl3rm7$r1d$1@dont-email.me> <8668311a-503f-46b6-909c-dcbfbfc5ce19@googlegroups.com> <nl41pc$apo$2@dont-email.me> <slrnnnc4cm.456.avl@login.logic.tuwien.ac.at> <e66db7c3-40cd-4df2-9e0e-9f23b0cb680c@googlegroups.com> <slrnnnivqf.456.avl@login.logic.tuwien.ac.at> <128e7e20-d311-413d-abbc-e885b34ae402@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 5 Jul 2016 16:23:10 -0000 (UTC)
Injection-Info: mx02.eternal-september.org; posting-host="cfefecc818af8c8edb17bddf4243dac6"; logging-data="3843"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18nZqzD8Gw7IR4zkaxUyEm5"
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.11; rv:45.0) Gecko/20100101 Thunderbird/45.1.1
In-Reply-To: <128e7e20-d311-413d-abbc-e885b34ae402@googlegroups.com>
Cancel-Lock: sha1:x1zJW6LGtQ58DCgCc5sbO+0yu+c=
Xref: csiph.com comp.lang.java.programmer:34758

Forgive my ignorance but can anyone suggest a newgroup or stackoverflow 
category or other URL that deals with proving programs correct?

If it helps, my goal is to prove that the following heuristically 
derived method nextGreater works on all trees, not just the ones I've 
tested it on.

/**
  * A Node is an element of a tree graph (acyclic). Each
  * Node xx can have up to two descendents, returned by
  * xx.getLeft and xx.getRight.
  * For any Node xx, if xx.getLeft is not null,
  * xx.getLeft().getParent()==xx.
  * For any Node xx, if xx.getRight is not null,
  * xx.getRight().getParent()==xx.
  * There is exactly one Node root for which
  * root.getParent is null.
  * For any Node xx, all keys of Nodes in the subtree
  * rooted at xx.getLeft are less than xx's key.
  * For any Node xx, all keys of Nodes in the subtree
  * rooted at xx.getRight are greater than xx's key.
  */
public abstract class Node {
public abstract Node getLeft();
public abstract Node getRight();
public abstract Node getParent();
/**
  * Return the tree node with the smallest key greater than
  * this node's key, if any. Do not rearrange any nodes.
  * @return the tree node with the smallest key greater than
  * this node's key, or <code>null</code> if no node in the
  * tree has a key greater than this node's key
  */
public Node nextGreater() {
   Node oneRightAllLeft=this.getRight();
   if (oneRightAllLeft!=null) {
     while (oneRightAllLeft.getLeft()!=null) {
       oneRightAllLeft=oneRightAllLeft.getLeft();
     }
     return oneRightAllLeft;
   }
   for (Node scan=this; ; ) {
     final Node elder=scan.getParent();
     if (elder==null || elder.getLeft()==scan) {
       return elder;
     }
     scan=elder;
   }
}
} // End class Node

--Mike Amling