14. Automatic program verification V: verification-oriented proof rules for arrays, records and pointers