Skip to content

Best practice to find class-level invariants for c++ classes #567

New issue
New issue
Open
Open
Best practice to find class-level invariants for c++ classes#567
@ChuyueSun

Description

@ChuyueSun
ChuyueSun
opened on Oct 17, 2024

I am trying to generate class-level invariants for c++ code.

This is the content of a c++ class avl_tree.h:

#include <functional>
#include <memory>
#include <vector>

typedef int T;

class AvlTree {

public:
  AvlTree();
  AvlTree(const AvlTree &t);
  AvlTree &operator=(const AvlTree &t);
  ~AvlTree();

  void insert(const T &v);
  void remove(const T &v);
  bool contains(const T &v);
  void clear();
  int height();
  int size();
  bool empty();
  std::vector<T> in_order_traversal() const;
  std::vector<T> pre_order_traversal() const;
  std::vector<T> post_order_traversal() const;

private:
  struct Node {
    T data;
    std::unique_ptr<Node> left;
    std::unique_ptr<Node> right;
    int balance_factor();
  };

  std::unique_ptr<Node> root;
  int n;

  void insert(const T &v, std::unique_ptr<Node> &p);
  void remove(const T &v, std::unique_ptr<Node> &p);
  bool contains(const T &v, std::unique_ptr<Node> &p);
  void clear(std::unique_ptr<Node> &p);
  int height(std::unique_ptr<Node> &p);
  void in_order_traversal(const std::unique_ptr<Node> &p,
                          std::vector<T> &v) const;
  void pre_order_traversal(const std::unique_ptr<Node> &p,
                           std::vector<T> &v) const;
  void post_order_traversal(const std::unique_ptr<Node> &p,
                            std::vector<T> &v) const;
  void balance(std::unique_ptr<Node> &p);
  void rotate_left(std::unique_ptr<Node> &p);
  void rotate_right(std::unique_ptr<Node> &p);
};

and avl_tree.cpp:

#include "avl_tree.h"
#include <stdexcept>

AvlTree::AvlTree() : root(nullptr), n(0) {}


AvlTree::AvlTree(const AvlTree &t) : root(nullptr), n(0) {
  for (auto v : t.in_order_traversal()) {
    insert(v);
  }
}

AvlTree &AvlTree::operator=(const AvlTree &t) {
  if (this != &t) {
    clear();
    for (auto v : t.in_order_traversal()) {
      insert(v);
    }
  }
  return *this;
}

 AvlTree::~AvlTree() { clear(); }

 void AvlTree::insert(const T &v) { insert(v, root); }

 void AvlTree::remove(const T &v) { remove(v, root); }

 bool AvlTree::contains(const T &v) {
  return contains(v, root);
}

void AvlTree::clear() { clear(root); }

int AvlTree::height() { return height(root); }

int AvlTree::size() { return n; }

bool AvlTree::empty() { return n == 0; }

std::vector<T> AvlTree::in_order_traversal() const {
  std::vector<T> v;
  in_order_traversal(root, v);
  return v;
}

std::vector<T> AvlTree::pre_order_traversal() const {
  std::vector<T> v;
  pre_order_traversal(root, v);
  return v;
}

std::vector<T> AvlTree::post_order_traversal() const {
  std::vector<T> v;
  post_order_traversal(root, v);
  return v;
}


void AvlTree::insert(const T &v, std::unique_ptr<Node> &p) {
  if (p == nullptr) {
    p = std::make_unique<Node>();
    p->data = v;
    n++;
  } else if (v < p->data) {
    insert(v, p->left);
  } else if (v > p->data) {
    insert(v, p->right);
  } else {
    throw std::invalid_argument("duplicate value");
  }
  balance(p);
}


void AvlTree::remove(const T &v, std::unique_ptr<Node> &p) {
  if (p == nullptr) {
    throw std::invalid_argument("value not found");
  } else if (v < p->data) {
    remove(v, p->left);
  } else if (v > p->data) {
    remove(v, p->right);
  } else {
    if (p->left == nullptr && p->right == nullptr) {
      p = nullptr;
    } else if (p->left == nullptr) {
      p = std::move(p->right);
    } else if (p->right == nullptr) {
      p = std::move(p->left);
    } else {
      std::unique_ptr<Node> &c = p->left;
      while (c->right != nullptr) {
        c = std::move(c->right);
      }
      p->data = c->data;
      c = std::move(c->left);
    }
    n--;
  }
  balance(p);
}


bool AvlTree::contains(const T &v, std::unique_ptr<Node> &p) {
  if (p == nullptr) {
    return false;
  } else if (v < p->data) {
    return contains(v, p->left);
  } else if (v > p->data) {
    return contains(v, p->right);
  } else {
    return true;
  }
}

 void AvlTree::clear(std::unique_ptr<Node> &p) {
  if (p != nullptr) {
    clear(p->left);
    clear(p->right);
    p = nullptr;
    n--;
  }
}

 int AvlTree::height(std::unique_ptr<Node> &p) {
  if (p == nullptr) {
    return 0;
  } else {
    return 1 + std::max(height(p->left), height(p->right));
  }
}


void AvlTree::in_order_traversal(const std::unique_ptr<Node> &p,
                                    std::vector<T> &v) const {
  if (p != nullptr) {
    in_order_traversal(p->left, v);
    v.push_back(p->data);
    in_order_traversal(p->right, v);
  }
}


void AvlTree::pre_order_traversal(const std::unique_ptr<Node> &p,
                                     std::vector<T> &v) const {
  if (p != nullptr) {
    v.push_back(p->data);
    pre_order_traversal(p->left, v);
    pre_order_traversal(p->right, v);
  }
}


void AvlTree::post_order_traversal(const std::unique_ptr<Node> &p,
                                      std::vector<T> &v) const {
  if (p != nullptr) {
    post_order_traversal(p->left, v);
    post_order_traversal(p->right, v);
    v.push_back(p->data);
  }
}

 void AvlTree::balance(std::unique_ptr<Node> &p) {
  if (p != nullptr) {
    if (height(p->left) - height(p->right) > 1) {
      if (height(p->left->left) >= height(p->left->right)) {
        rotate_right(p);
      } else {
        rotate_left(p->left);
        rotate_right(p);
      }
    } else if (height(p->right) - height(p->left) > 1) {
      if (height(p->right->right) >= height(p->right->left)) {
        rotate_left(p);
      } else {
        rotate_right(p->right);
        rotate_left(p);
      }
    }
  }
}

void AvlTree::rotate_left(std::unique_ptr<Node> &p) {
  std::unique_ptr<Node> r = std::move(p->right);
  p->right = std::move(r->left);
  r->left = std::move(p);
  p = std::move(r);
}

void AvlTree::rotate_right(std::unique_ptr<Node> &p) {
  std::unique_ptr<Node> l = std::move(p->left);
  p->left = std::move(l->right);
  l->right = std::move(p);
  p = std::move(l);
}

I am using test_avl_tree.cpp to execute unit tests:

#include <iostream>
#include "avl_tree.h"  // Include class header file

int main() {
    // Test Case 1
    {
        /* Test 1: Basic insertions and traversals */
AvlTree tree;
tree.insert(10);
tree.insert(20);
tree.insert(5);
tree.in_order_traversal();
tree.pre_order_traversal();
tree.post_order_traversal();
    }

    // Test Case 2
    {
        /* Test 2: Checking size, height, and empty status */
AvlTree tree;
tree.insert(10);
tree.insert(20);
tree.insert(5);
tree.size();
tree.height();
tree.empty();
    }

    // Test Case 3
    {
        /* Test 3: Removing elements and checking tree properties */
AvlTree tree;
tree.insert(10);
tree.insert(20);
tree.insert(5);
tree.remove(10);
tree.size();
tree.height();
tree.contains(10);
tree.contains(20);
tree.contains(5);
    }

    // Test Case 4
    {
        /* Test 4: Inserting duplicate values */
AvlTree tree;
tree.insert(10);
try {
    tree.insert(10);
} catch (const std::invalid_argument &e) {
    // Expected exception for duplicate value
}
    }

    // Test Case 5
    {
        /* Test 5: Removing non-existent values */
AvlTree tree;
tree.insert(10);
try {
    tree.remove(20);
} catch (const std::invalid_argument &e) {
    // Expected exception for non-existent value
}
    }

    // Test Case 6
    {
        /* Test 6: Clearing the tree */
AvlTree tree;
tree.insert(10);
tree.insert(20);
tree.insert(5);
tree.clear();
tree.size();
tree.height();
tree.empty();
    }

    // Test Case 7
    {
        /* Test 7: Copy constructor */
AvlTree tree1;
tree1.insert(10);
tree1.insert(20);
tree1.insert(5);
AvlTree tree2 = tree1;
tree2.size();
tree2.height();
tree2.contains(10);
tree2.contains(20);
tree2.contains(5);
    }

    // Test Case 8
    {
        /* Test 8: Assignment operator */
AvlTree tree1;
tree1.insert(10);
tree1.insert(20);
tree1.insert(5);
AvlTree tree2;
tree2 = tree1;
tree2.size();
tree2.height();
tree2.contains(10);
tree2.contains(20);
tree2.contains(5);
    }

    // Test Case 9
    {
        /* Test 9: Complex sequence of operations */
AvlTree tree;
tree.insert(10);
tree.insert(20);
tree.insert(5);
tree.insert(15);
tree.insert(25);
tree.remove(20);
tree.insert(30);
tree.remove(10);
tree.size();
tree.height();
tree.in_order_traversal();
tree.pre_order_traversal();
tree.post_order_traversal();
tree.clear();
tree.empty();
    }

    // Test Case 10
    {
        /* Test 10: Edge case with single element */
AvlTree tree;
tree.insert(10);
tree.size();
tree.height();
tree.contains(10);
tree.remove(10);
tree.size();
tree.height();
tree.empty();
    }

    return 0;
}

Then I run g++ -o avl test_avl_tree.cpp avl_tree.cpp -gdwarf-2 -no-pie
and then ~/daikon-5.8.20/scripts/kvasir-dtrace ./avl

==3676549== kvasir-5.8.20, C/C++ Language Front-End for Daikon with DynComp comparability analysis tool.
==3676549== Copyright (C) 2007-2022, University of Washington CSE PLSE Group
==3676549== Using Valgrind-3.19.0.Fjalar and LibVEX; rerun with -h for copyright info
==3676549== Command: ./avl
==3676549== 
  Start garbage collecting (next tag = 10000001, total assigned = 10000000)
   Done garbage collecting (next tag = 6013291, total assigned = 10000000)
MISMATCHED on exit_function! f: ..main() !=  AvlTree.remove(int const&, std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&)
DetectedEntryIP: 0x402543 - AssumedEntryIP: 0x401326
DetctedExitIP: 0x402815 - AssumedExitIp: 0x401c5d
==3676549== 
==3676549== For lists of detected and suppressed errors, rerun with: -s
==3676549== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)

and then java -cp $DAIKONDIR/daikon.jar daikon.Daikon --config_option daikon.derive.Derivation.disable_derived_variables=true daikon-output/avl.decls daikon-output/avl.dtrace > daikon.txt
The content of daikon.txt is

Daikon version 5.8.20, released May 14, 2024; http://plse.cs.washington.edu/daikon.
Reading declaration files .
(read 1 decls file)
Processing trace data; reading 1 dtrace file:

No return from procedure observed 5 times.  Unmatched entries are ignored!
Unterminated calls:
  AvlTree.insert(int const&) : 1 invocation
  AvlTree.insert(int const&, std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&) : 1 invocation
  AvlTree.remove(int const&) : 1 invocation
  AvlTree.remove(int const&, std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&) : 2 invocations
End of report for procedures not returned from.  Unmatched entries are ignored!

===========================================================================
..main():::EXIT
return == 0
===========================================================================
..operator new(unsigned long, void*):::ENTER
unnamed_parameter0xd4d0 == 4
__p != null
===========================================================================
..operator new(unsigned long, void*):::EXIT
return == orig(__p)
return != null
===========================================================================
AvlTree.AvlTree():::ENTER
this->n >= 0
===========================================================================
AvlTree.AvlTree():::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this->n == 0
this->n <= orig(this->n)
===========================================================================
AvlTree.AvlTree(AvlTree const&):::ENTER
this has only one value
this[0] has only one value
this->root has only one value
this->root._M_t has only one value
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t has only one value
this->n == 0
t has only one value
t.root has only one value
t.root._M_t has only one value
t.root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t has only one value
t.n == 3
===========================================================================
AvlTree.AvlTree(AvlTree const&):::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
t.root == orig(t.root)
t.root._M_t == orig(t.root._M_t)
t.root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(t.root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
t.n == orig(t.n)
this[0] has only one value
this->root has only one value
this->root._M_t has only one value
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t has only one value
this->n == 3
t.root has only one value
t.root._M_t has only one value
t.root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t has only one value
t.n == 3
===========================================================================
AvlTree.balance(std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&):::ENTER
this != null
this[0] != null
this->root != null
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p != null
p._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] elements != null
===========================================================================
AvlTree.balance(std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&):::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this->n == orig(this->n)
p._M_t == orig(p._M_t)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl)
this[0] != null
this->root != null
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] elements != null
===========================================================================
AvlTree.clear():::ENTER
this != null
this[0] != null
this->root != null
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
this->n >= 0
===========================================================================
AvlTree.clear():::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this[0] != null
this->root != null
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
this->n == 0
this->n <= orig(this->n)
===========================================================================
AvlTree.clear(std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&):::ENTER
this != null
this[0] != null
this->root != null
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
this->n >= 0
p != null
p._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] elements != null
===========================================================================
AvlTree.clear(std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&):::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
p._M_t == orig(p._M_t)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl)
this[0] != null
this->root != null
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
this->n >= 0
p._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl == null
this->n <= orig(this->n)
===========================================================================
AvlTree.contains(int const&):::ENTER
this has only one value
this[0] has only one value
this->root has only one value
this->root._M_t has only one value
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t has only one value
this->n one of { 1, 2, 3 }
v one of { 5, 10, 20 }
===========================================================================
AvlTree.contains(int const&):::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this->n == orig(this->n)
this[0] has only one value
this->root has only one value
this->root._M_t has only one value
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t has only one value
this->n one of { 1, 2, 3 }
===========================================================================
AvlTree.contains(int const&, std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&):::ENTER
this has only one value
this != null
this[0] has only one value
this[0] != null
this->root has only one value
this->root != null
this->root._M_t has only one value
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t has only one value
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
this->n one of { 1, 2, 3 }
v one of { 5, 10, 20 }
p != null
p._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] elements != null
===========================================================================
AvlTree.contains(int const&, std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&):::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this->n == orig(this->n)
p._M_t == orig(p._M_t)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[])
this[0] has only one value
this[0] != null
this->root has only one value
this->root != null
this->root._M_t has only one value
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t has only one value
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
this->n one of { 1, 2, 3 }
p._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] elements != null
===========================================================================
AvlTree.empty():::ENTER
this->n one of { 0, 3 }
===========================================================================
AvlTree.empty():::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this->n == orig(this->n)
this->n one of { 0, 3 }
===========================================================================
AvlTree.height():::ENTER
===========================================================================
AvlTree.height():::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this->n == orig(this->n)
===========================================================================
AvlTree.height(std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&):::ENTER
this != null
this[0] != null
this->root != null
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p != null
p._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] elements != null
===========================================================================
AvlTree.height(std::unique_ptr<AvlTree::Node, std::default_delete<AvlTree::Node> >&):::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this->n == orig(this->n)
p._M_t == orig(p._M_t)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl)
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] == orig(p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[])
this[0] != null
this->root != null
this->root._M_t != null
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Tuple_impl<1, std::default_delete<AvlTree::Node> >._Head_base<1, std::default_delete<AvlTree::Node>, true>._M_head_impl != null
p._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t._Tuple_impl<0, AvlTree::Node*, std::default_delete<AvlTree::Node> >._Head_base<0, AvlTree::Node*, false>._M_head_impl[] elements != null
return >= 0
===========================================================================
AvlTree.in_order_traversal() const:::ENTER
this->n one of { 3, 4 }
===========================================================================
AvlTree.in_order_traversal() const:::EXIT
this[0] == orig(this[0])
this->root == orig(this->root)
this->root._M_t == orig(this->root._M_t)
this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t == orig(this->root._M_t.__uniq_ptr_impl<AvlTree::Node, std::default_delete<AvlTree::Node> >._M_t)
this->n == orig(this->n)
return._Vector_base<int, std::allocator<int> >._M_impl._Vector_impl_data._M_start == return._Vector_base<int, std::allocator<int> >._M_impl._Vector_impl_data._M_finish
return._Vector_base<int, std::allocator<int> >._M_impl._Vector_impl_data._M_start[] == return._Vector_base<int, std::allocator<int> >._M_impl._Vector_impl_data._M_finish[]
this->n one of { 3, 4 }
return has only one value
return._Vector_base<int, std::allocator<int> >._M_impl has only one value
===========================================================================
..........rest of the file

To qualify as a class-level invariant, this invariant must appear in every ENTER and EXIT point of every public method. So my plan is to parse out these invariants.

Am I using Daikon correctly? Does my method make sense? Are there any existing options in place for finding such invariants?

The output of java -version, and the operating system version.

openjdk version "11.0.24" 2024-07-16. 
OpenJDK Runtime Environment (build 11.0.24+8-post-Ubuntu-1ubuntu322.04)  
OpenJDK 64-Bit Server VM (build 11.0.24+8-post-Ubuntu-1ubuntu322.04, mixed mode, sharing)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions