Boogie program basic concept

a program is several top level declarations, including function, procedure, implementation .etc.

procedure has ensurance, requirements, etc.

implementation implements the procedure.