In the world of Program Synthesis, bottom-up enumeration with observational equivalence is a common approach for generating programs. However, classical observational equivalence has a strong assumption that all generated programs are pure, a constraint that is particularly limiting for object-oriented languages.
We introduce Concrete Graph Logic, an extension of Hoare Logic, to address this limitation. In this logic, we represent the program context and its objects using Object Graphs and introduce a new rule called the embedding rule, which replaces the consequence rule in Hoare Logic.
This rule defines when an embedding of pre-condition and post-condition graphs in a larger graph maintains the validity of the Hoare triplet. Using this rule and the standard composition rule, we can compose two Hoare triplets with compatible conditions.
We also present an algorithm that, given two Hoare triplets, finds a valid embedding that allows for their composition, if one exists. This algorithm is implemented in Ruse, a new program synthesizer capable of generating mutating object-oriented JavaScript programs.