Long story short (for more detail, see the lecture): The problematic commands are loops. So, if you write:

method Easy(..)
  requires Phi;
  ensures Psi;
{
  P1;
  while ( C )
     invariant I;
  {
    P2;
  }
  P3;
}

Dafny tries to prove three separate implications:

 Phi [P1] => I
 (I and C) [P2] => I
 (I and not C) [P3] => Psi

If it fails in 1., it writes, "This loop invariant might not hold on entry."
If it fails in 2., it writes, "This loop invariant might not be maintained by the loop."
If it fails in 3., it writes, "A postcondition might not hold on this return path."

F [Px] stands for modification of property F by the program part Px (for more detail, see the lecture).