Skip to content

Commit dcfe055

Browse files
committed
Added files for work on new ideas
1 parent d5222aa commit dcfe055

File tree

2 files changed

+95
-0
lines changed

2 files changed

+95
-0
lines changed

article/defs.tex

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
% for typesetting 'program' like words
2+
\newcommand{\prg}[1]{\texttt{#1}}
3+
4+
% short-hand for program transformation
5+
\newcommand{\pt}{\mathit{pt}}
6+
7+
% application of program transformation to a term
8+
\newcommand{\apply}[2]{\mathit{apply}(#1,#2)}
9+
10+
% edit-distance
11+
\newcommand{\edist}[2]{\delta(#1,#2)}
12+
13+
% safety of program transformation
14+
\newcommand{\partof}[2]{#1\preceq #2}

article/idea.tex

+81
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
\documentclass{article}
2+
3+
% often used definitions
4+
\input{defs}
5+
6+
7+
\title{\prg{spdiff} revisited}
8+
9+
\begin{document}
10+
\maketitle
11+
12+
\section{Recap}
13+
14+
% Something about the definitions we had.
15+
Here's a short recap of the definitions.
16+
17+
\paragraph{Part-of}
18+
19+
We have a notion of when a semantic patch, $\pt$ is ``part of'' with
20+
respect to a pair of terms representing an old and a new version of a
21+
program, $(t,t')$:
22+
23+
\[\forall \pt,t,t':
24+
\partof{\pt}{(t,t')} \iff \exists t'':
25+
\apply{\pt}{t}=t'' \wedge \edist{t}{t''} + \edist{t''}{t'} = \edist{t}{t'}
26+
\]
27+
28+
The intuition is that $\pt$ should somehow perform part of the
29+
transformation of $t$ into $t'$. (Confusingly, I sometimes also called
30+
this safety.)
31+
32+
We can also extend this definition to work for entire changesets by
33+
(overloading the ``part-of'' notation from before)
34+
35+
\[\forall \pt, C:
36+
\partof{\pt}{C} \iff \forall(t,t') \in C:\partof{\pt}{(t,t')}
37+
\]
38+
39+
\paragraph{Sub-patch}
40+
41+
We also defined a notion of when one semantic patch, $\pt'$ subsumes
42+
another, $\pt$. We then say that $\pt$
43+
is a subpatch of $\pt'$:
44+
45+
\[\forall \pt,\pt':
46+
\partof{\pt}{\pt'} \iff \forall t,t' :
47+
\partof{\pt'}{(t,t')} \wedge
48+
\apply{\pt'}{t} = t'' \wedge
49+
\partof{\pt}{(t,t'')}
50+
\]
51+
52+
An issue with the above
53+
54+
\section{Issues}
55+
56+
% Something about the issues with the previous solution.
57+
58+
The main issue I think is related to the threshold notion. Here's a
59+
list of issues that I've thought of so far:
60+
61+
\begin{enumerate}
62+
\item How can one select a threshold? The current approach is
63+
something like, trying to run \prg{spdiff} with threshold $n$ and if
64+
the results look strange, rerun \prg{spdiff} with a different
65+
threshold. If the results look to detailed, rerun with higher
66+
threshold and if the results does not include the changes one
67+
thought, rerun with a lower threshold in the hope that it will now
68+
be allowed to be included. In both cases In both cases it seems to
69+
me that one already has some idea of who the resulting semantic
70+
patch should look which begs the question: why not just write the
71+
semantic patch by hand then?
72+
\item When using a relatively lower threshold, one can get two
73+
semantic patches which are not in
74+
\end{enumerate}
75+
76+
\section{Suggestion}
77+
78+
% The great new idea!
79+
80+
81+
\end{document}

0 commit comments

Comments
 (0)