Dafny verification fails "post condition might not hold"

Question

i am new here (my first question) We are supposed to use a given code from a website and convert it into dafny code. The code logic itself is supposedly good. When i try to convert the code in dafny it complains that the postconditions might not hold:

it specifically complains about the following lines:

ensures isMaxHeap(heapifiedArray) in the method BuildMaxHeap ensures maxHeapPrperty(arr, i) == true in the method MaxHeapify assert maxHeapPrperty(arr, i); in the method MaxHeapify

What am i doing wrong and how can i rectify this? I attempted multiple times to rewrite the maxHeapPrperty method thinking maybe its the crux of the issue. But, it did not work.

I am pretty new to dafny so I am sorry if this question is a little too basic, i am trying to learn, i hit a brick wall and i cannot seem to be to crack this.

predicate isMaxHeap(arr : array<nat>)
requires arr.Length >= 0
reads arr
{
  forall i : int :: 0 <= i < arr.Length/2-1 ==> maxHeapPrperty(arr, i)
}

predicate maxHeapPrperty(arr : array<nat>, i : int)
requires arr.Length >= 0
requires 0 <= i < arr.Length
reads arr
{
  if (2*i +2 >= arr.Length && 2*i +1 >= arr.Length) then true
  else if (2*i +2 >= arr.Length) then arr[i] >= arr[2*i +1]
  else arr[i] >= arr[2*i +1] && arr[i] >= arr[2*i +2]
  
}
method BuildMaxHeap(arr : array<nat>) returns(heapifiedArray : array<nat>)
requires arr.Length > 3
modifies arr
ensures isMaxHeap(heapifiedArray)
{
  var i := (arr.Length/2)-1;
  while (2 == 0) {

          MaxHeapify(arr, i);
    i := i-1;

  }
  heapifiedArray := arr;
}



method MaxHeapify(arr: array<nat>, i: int)
  requires arr.Length > 0
  requires 0 <= i < arr.Length
  modifies arr
  decreases arr.Length - i
  ensures maxHeapPrperty(arr, i) == true
{
  var largest: int := i; // Initialize largest as root
  var l: int := 2 * i + 1; // left = 2*i + 1
  var r: int := 2 * i + 2; // right = 2*i + 2


  if l < arr.Length && arr[l] > arr[largest] {
    largest := l;
  }


  if r < arr.Length && arr[r] > arr[largest] {
    largest := r;
  }

  assert largest == i || (largest == l && arr[largest] >= arr[i]) || (largest == r && arr[largest] >= arr[i]);


  if largest != i {
    swap(arr, i, largest);


    MaxHeapify(arr, largest);

  }

  assert maxHeapPrperty(arr, i);
}

method swap(arr : array<nat>, i : int, j : int) 
requires arr.Length > 0
requires 0 <= i < arr.Length
requires 0 <= j < arr.Length
modifies arr
ensures arr[j] == old(arr[i])
ensures arr[i] == old(arr[j])
{
  var temp := arr[i];
  arr[i] := arr[j];
  arr[j] := temp;

}

I tried to convert a code from Java to dafny, the code's logic is supposed to be sound, The code does indeed produce a maxHeap, however when i try to inssert the preconditions and the post conditions, it complains, i do not know why.