package assignment2;

import be.ac.ua.ansymo.adbc.annotations.invariant;

@invariant("$this.isBalanced() == true")
public class BalancedBinTree extends BinTree {

	public BalancedBinTree(long id) {
		super(id);
	}

	public boolean isBalanced() {
		int lh = 0;
		int rh = 0;
		
		if (this.getLeft() != null) {
			lh = this.getLeft().height();
		}
		if (this.getRight() != null) {
			rh = this.getRight().height();
		}
		if (Math.abs(lh - rh) < 2) {
			return true;
		}
		
		return false;
	}
	
}

@@ -78,16 +78,27 @@
 variant(
+%7B%22$super%22, 
 %22$this.i
@@ -117,16 +117,17 @@
 == true%22
+%7D
 )%0Apublic
@@ -203,16 +203,16 @@
 g id) %7B%0A
+
 %09%09super(
@@ -222,284 +222,8 @@
 ;%0A%09%7D
-%0A%0A%09public boolean isBalanced() %7B%0A%09%09int lh = 0;%0A%09%09int rh = 0;%0A%09%09%0A%09%09if (this.getLeft() != null) %7B%0A%09%09%09lh = this.getLeft().height();%0A%09%09%7D%0A%09%09if (this.getRight() != null) %7B%0A%09%09%09rh = this.getRight().height();%0A%09%09%7D%0A%09%09if (Math.abs(lh - rh) %3C 2) %7B%0A%09%09%09return true;%0A%09%09%7D%0A%09%09%0A%09%09return false;%0A%09%7D
 %0A%09%0A%7D

Bring method into superclass.