A Characterization of Program Equivalence in Terms of Hoare’s Logic

We discuss the equivalence of simple while-programs S1 and S2 in all datatypes that implement a specification (Σ,E). A sufficientcondition is that S1 and S2 are indistinguishable in all program logics HL(Σ’,E) for Σ’ ⊃; Σ. A necessary condition is that for each refinement (Σ’,E’) of (Σ,E) another refinement (Σ*,E*) of (Σ’ ,E’) exists such that S1 and S2 cannot be distinguished in HL(Σ*,E*).