Array_Slices definitions - Verifast Java

I'm having a course in University named "Construction and Verification of Software" and We've started the course with a language named Dafny and now we are using Verifast in Java to verify our Software.

The Professor gave us some slides and some code to build a bug-free program to represent a Bank and its Bank Account's.

There are some definitions in the code and I'm still not getting it after some research, because the lack of documentation on the internet.

Below there is some code that I'm having some doubts.

I Understand the AccountP invariant.

/*@
   predicate AccountP(unit a,BankAccount c; int n) = c != null &*& AccountInv(c,n,?m);
@*/

/*@
   predicate BankInv(Bank bk; int n, int c) = 
     bk.nelems |-> n &*& 
     bk.capacity |-> c &*& 
     c > 0 &*&
     bk.store |-> ?accountArray &*&
     accountArray != null &*&
     accountArray.length == c &*&
     0 <= n &*& n<=c &*& 
     array_slice_deep(accountArray, 0, n, AccountP, unit,_,?bs) &*&
     array_slice(accountArray, n, c,?rest) &*& all_eq(rest, null) == true ;
 @*/

In some methods of the given code ( in addNewAccount() for example) it appears these "functions" that I don't know for what they are used for. These are the following:

//@ array_slice_split(store, nelems,nelems+1);
//@ array_slice_deep_close(store, nelems, AccountP, unit);

Basically I need some help on the definitions on: array_slice, array_slice_deep, array_slice_deep_close and array_slice_split to move on the program.

It would be great if someone could help me.

Thanks.