<p>You could have directly asked about the problem of correct factoring!</p>

<ul>
<li><a href="http://www.dsi.unive.it/~cortesi/paperi/vmcai06.pdf%E2%80%8E" rel="nofollow">Semantic Hierarchy Refactoring by Abstract Interpretation</a> Logozzo and Cortesi, 2004. (looks at how to merge two class hierarchies by refactoring correctly)</li>
<li><a href="http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&amp;id=BannwartMueller06.pdf" rel="nofollow">Changing Programs Correctly: Refactoring with Specifications</a>, Banwart and Mueller, 2006. (One of the first papers looking at the properties preserved by refactoring.)</li>
<li><a href="http://www.sciencedirect.com/science/article/pii/S0167642309001300" rel="nofollow">Sound refactorings</a>, Cornelio, Cavalcanti, Sampaio, 2010. (a reasoning framework based on weakest preconditions)</li>
<li><a href="http://kar.kent.ac.uk/23975/" rel="nofollow">Verification of Refactorings in Isabelle/HOL</a>, Sultana, 2008 (title says it all)</li>
<li><a href="http://research.microsoft.com/apps/pubs/default.aspx?id=170382" rel="nofollow">An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts</a>, Cousot, Cousot, Logozzo, Barnett. 2012. (A semantics based refactoring implemented in some Microsoft tools)</li>
</ul>

<p>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.</p>

CC BY-SA 3.0
2013-07-11T18:29:49.563Z
2013-07-11T18:29:49.563Z
Vijay D
<p>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.</p>

<p>In terms of the state of the art, I think <a href="http://www21.in.tum.de/~lammich/pub/autoref.pdf" rel="nofollow">Lammich's tool</a> in Isabelle/HOL has been used successfully in at least two significant developments (a verification of Hopcroft's algorithm by <a href="http://www21.in.tum.de/~lammich/pub/itp12.pdf" rel="nofollow">Lammich and Tuerk</a>, and a verified implementation of an LTL model checker by <a href="http://www21.in.tum.de/~lammich/pub/verified_ltl_paper.pdf" rel="nofollow">Esparza, Lammich et al</a>).  Ironically, I was also reading <a href="http://wiki.portal.chalmers.se/cse/uploads/ForMath/refinements_for_free.pdf" rel="nofollow">this paper</a> this morning, about a similar tool, newly developed, in Coq, courtesy of the dependent_types subreddit on Reddit.</p>

CC BY-SA 3.0
2013-06-26T12:27:40.457Z
Good job mentioning refinement! I recommend Morgan's classic "Programming from Specifications" (http://www.cs.ox.ac.uk/publications/books/PfS/) which is somewhat easy to understand, and Back's "Refinement Calculus" (http://www.amazon.com/dp/0387984178), which is unfortunately less accessible.
Malte Schwerhoff
CC BY-SA 3.0
2013-06-26T09:15:01.970Z
2013-06-26T09:15:01.970Z
Dominic Mulligan
<p>Thank you all for you inputs and ideas. I think Opdyke 1992 thesis is also very close to what I was searching for <a href="http://www.laputan.org/pub/papers/opdyke-thesis.pdf" rel="nofollow">http://www.laputan.org/pub/papers/opdyke-thesis.pdf</a></p>

<p>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 <a href="http://wiki.eclipse.org/images/b/be/PTPUserDev2012_Ruegg_Refactoring.pdf" rel="nofollow">http://wiki.eclipse.org/images/b/be/PTPUserDev2012_Ruegg_Refactoring.pdf</a> on how CDT (C++ Development Tookit for Eclipse) performs refactoring, and they cite [Opdyke 1992] and [Opdyke 1999] (probably this <a href="http://st-www.cs.illinois.edu/users/opdyke/wfo.990201.refac.html" rel="nofollow">http://st-www.cs.illinois.edu/users/opdyke/wfo.990201.refac.html</a>).</p>

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

CC BY-SA 3.0
2013-07-11T13:50:58.037Z
2013-07-11T13:50:58.037Z
Claudio
<p>On field of interest could be <em>relational verification</em> as, for example, presented in <a href="http://research.microsoft.com/apps/video/dl.aspx?id=191262" rel="nofollow">this video</a> or in <a href="http://software.imdea.org/~jmcrespo/docs/FM2011.pdf" rel="nofollow">this paper</a>. 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.</p>

<p>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.</p>

CC BY-SA 3.0
2013-06-26T07:16:30.567Z
2013-06-26T07:16:30.567Z
Malte Schwerhoff
<p>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.</p>

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

<p>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.</p>

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

CC BY-SA 3.0
2013-06-25T15:14:35.520Z
This is a generalisation of the question of compiler correctness.
Charles Stewart
CC BY-SA 3.0
2013-06-25T20:13:22.370Z
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](http://en.wikipedia.org/wiki/Automated_theorem_proving) and transformations that preserve equality.
vzn
<reference-request><lo.logic><property-testing>
What is the state of the art in theory of "Software transformations preserving behavior"?
Claudio
# What is the state of the art in theory of "Software transformations preserving behavior"?

(Asked by: username_0 on 2013-06-25)

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.

**Tags:** reference-request, lo.logic, property-testing
> **Comments:**
> **username_1**: This is a generalisation of the question of compiler correctness.  
> **username_2**: 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](http://en.wikipedia.org/wiki/Automated_theorem_proving) and transformations that preserve equality.  

---

## 4 answers

### Answer by username_3 on 2013-07-11. Score: 3

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

* [Semantic Hierarchy Refactoring by Abstract Interpretation](http://www.dsi.unive.it/~cortesi/paperi/vmcai06.pdf%E2%80%8E) Logozzo and Cortesi, 2004. (looks at how to merge two class hierarchies by refactoring correctly)
* [Changing Programs Correctly: Refactoring with Specifications](http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=BannwartMueller06.pdf), Banwart and Mueller, 2006. (One of the first papers looking at the properties preserved by refactoring.)
* [Sound refactorings](http://www.sciencedirect.com/science/article/pii/S0167642309001300), Cornelio, Cavalcanti, Sampaio, 2010. (a reasoning framework based on weakest preconditions)
* [Verification of Refactorings in Isabelle/HOL](http://kar.kent.ac.uk/23975/), Sultana, 2008 (title says it all)
* [An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts](http://research.microsoft.com/apps/pubs/default.aspx?id=170382), Cousot, Cousot, Logozzo, Barnett. 2012. (A semantics based refactoring implemented in some Microsoft tools)

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.


---

### Answer by username_4 on 2013-06-26. Score: 3

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](http://www21.in.tum.de/~lammich/pub/autoref.pdf) in Isabelle/HOL has been used successfully in at least two significant developments (a verification of Hopcroft's algorithm by [Lammich and Tuerk](http://www21.in.tum.de/~lammich/pub/itp12.pdf), and a verified implementation of an LTL model checker by [Esparza, Lammich et al](http://www21.in.tum.de/~lammich/pub/verified_ltl_paper.pdf)). Ironically, I was also reading [this paper](http://wiki.portal.chalmers.se/cse/uploads/ForMath/refinements_for_free.pdf) this morning, about a similar tool, newly developed, in Coq, courtesy of the dependent\_types subreddit on Reddit.

> **Comments:**
> **username_5**: Good job mentioning refinement! I recommend Morgan's classic "Programming from Specifications" (http://www.cs.ox.ac.uk/publications/books/PfS/) which is somewhat easy to understand, and Back's "Refinement Calculus" (http://www.amazon.com/dp/0387984178), which is unfortunately less accessible.  

---

### Answer by username_0 on 2013-07-11. Score: 2

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! :)


---

### Answer by username_5 on 2013-06-26. Score: 2

On field of interest could be *relational verification* as, for example, presented in [this video](http://research.microsoft.com/apps/video/dl.aspx?id=191262) or in [this paper](http://software.imdea.org/~jmcrespo/docs/FM2011.pdf). 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.


---

