Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Open
ChuyueSun opened this issue Oct 17, 2024 · 0 comments
Open

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

ChuyueSun opened this issue Oct 17, 2024 · 0 comments

Comments

@ChuyueSun
Copy link

ChuyueSun commented Oct 17, 2024 •
edited
Loading

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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@ChuyueSun