This video shows how to proving reachability property of push method .The method contract is specified in JML (not shown in this video).