7
$\begingroup$

I am interested in the field that could perhaps be referred to as "Automated Refactory" or "Preservation of Software Properties" after a transformation/change/refactory.

Saying we have an instruction/set of instructions I with some functional property P and some transformation T so that I' = T(I). Is there any research/work/papers that models P (just some properties, a group of, ...) and preservation/changes of those properties between I and I' for a set of transformations T?

First of all, what is the correct name for this fiels? Then, I would like to know if a theory to model this problem exists, which one is the most used (or the most referred to) and if any application of that system/metric/model (libraries, IDE plugins, ...) has been released.

If you can give any name, paper, ... whatever that is considered "fundamental" in this field, I will dig into this on my own.

$\endgroup$
  • 2
    $\begingroup$ This is a generalisation of the question of compiler correctness. $\endgroup$ – Charles Stewart Jun 25 '13 at 15:14
  • $\begingroup$ can you narrow down the transformation property? it is not too commonly studied in general it would seem but there are special cases. a basic angle is the property of code/register optimization in compilers. another angle is "automated refactoring" that happens in some IDEs eg eclipse, which is invoked by developers manually on candidate sections of code. there is also an analogy to automated theorem proving and transformations that preserve equality. $\endgroup$ – vzn Jun 25 '13 at 20:13
3
$\begingroup$

I think what you are looking for, in the context of verified transformations in a proof assistant, is known as "refinement", wherein a very-high level, inefficient implementation of some algorithm is gradually refined down into an efficient, low-level implementation, proving that the transformations preserve certain properties along the way. Various tools have been developed to help the user do this without being overcome by tedious book keeping.

In terms of the state of the art, I think Lammich's tool in Isabelle/HOL has been used successfully in at least two significant developments (a verification of Hopcroft's algorithm by Lammich and Tuerk, and a verified implementation of an LTL model checker by Esparza, Lammich et al). Ironically, I was also reading this paper this morning, about a similar tool, newly developed, in Coq, courtesy of the dependent_types subreddit on Reddit.

$\endgroup$
3
$\begingroup$

You could have directly asked about the problem of correct factoring!

Let me know if this is what you were looking for. Your original question is very general in scope, so it was difficult to know what was precisely required.

$\endgroup$
2
$\begingroup$

On field of interest could be relational verification as, for example, presented in this video or in this paper. The basic idea of relation verification is, that you prove some properties about a "simple" version of a program, and then show that a "hard" version of the same program behaves shows the same behaviour as the easy program. In a sense, you use the easy version as a specification for the hard one. "easy" could be unoptimised, sequential or functional, and "hard" could then be optimised, concurrent or imperative.

Relational verification is sometimes also referred to as "relational reasoning". If you search for "relational verification", it is very likely that you'll also find resources about relational dabatases and relational domains as used in abstract interpretation.

$\endgroup$
2
$\begingroup$

Thank you all for you inputs and ideas. I think Opdyke 1992 thesis is also very close to what I was searching for http://www.laputan.org/pub/papers/opdyke-thesis.pdf

Basically, I tried the bottom-up approach asking myself "How do Eclipse teams check for preconditions and postconditions afer you perform a refactoring?" I came into this article http://wiki.eclipse.org/images/b/be/PTPUserDev2012_Ruegg_Refactoring.pdf on how CDT (C++ Development Tookit for Eclipse) performs refactoring, and they cite [Opdyke 1992] and [Opdyke 1999] (probably this http://st-www.cs.illinois.edu/users/opdyke/wfo.990201.refac.html).

Still searching interesting material related to this, so if anyone has other articles or names to share, it is more than welcome! :)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.