Rely/Guarantee Refinement Calculus' blog

On my PhD, I worked on the mechanisation of a refinement calculus to supports derivation of programs specified using rely-guarantee. Yesterday, while preparing a manuscript to FACJ, I decided to start a blog about the theory that I worked on during the PhD. The blog can be accessed here.


The thesis:

My thesis is entitled Mechanising an Algebraic Rely-Guarantee Refinement Calculus. Refinement calculus can be thought as programming methodologies where design decisions are formally recorded. They generally consist on a collection of refactoring templates that can be applied by a programmer to transform mathematical specifications into executable code. The benefit of using this approach is that it guarantees that the implementation constructed by the programmer does exactly what the mathematical specification demands. This methodology results in software that is correct-by-construction, eliminating potential costs in post-production due to bugs. In my thesis this approach is illustrated via the derivation of non-trivial algorithms taken from the literature on refinement calculus.