A rule-based verification strategy for array manipulating programs