Quelle bst.vdmpp Sprache: VDM

class BinarySearchTree is subclass of Tree

  functions

    public
    isBst : Tree`tree -> bool
    isBst (t) ==
      cases t:
        <Empty> -> true,
        mk_node(lt,v,rt) ->
           (forall n in set lt.nodes() & n.nval <= v) and
           (forall n in set rt.nodes() & v <= n.nval) and
           isBst(lt.gettree()) and isBst(rt.gettree())
      end

  operations

    BinarySearchTree_inv : () ==> bool
    BinarySearchTree_inv () ==
      return(isBst(root));

    public
    Insert : int ==> ()
    Insert (x) ==
      (dcl curr_node : Tree := self;

       while not curr_node.isEmpty() do
         if curr_node.rootval() < x
         then curr_node := curr_node.rightBranch()
         else curr_node := curr_node.leftBranch();
       curr_node.addRoot(x);
       )

end BinarySearchTree
class BalancedBST is subclass of BinarySearchTree

  values

  v = 1

end BalancedBST

quality97%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.