CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Generic Diff3 for Algebraic Datatypes

Marco Vassena (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Proceeding TyDe 2016, Proceedings of the 1st International Workshop on Type-Driven Development p. 62-71. (2016)
[Konferensbidrag, refereegranskat]

Many version control systems, including Git and Mercurial, rely on diff3 to merge different revisions of the same file. More precisely diff3 automatically merges two text files, given a common base version, comparing them line by line and raising conflicts when the changes made are irreconcilable. The program ignores the actual structure of the data stored in the files, hence it might generate spurious conflicts, which must be manually resolved by the user. In this paper, we present a state-based, three-way, persistent, data-type generic diff3 algorithm whose increased precision in detecting changes reduces the number of false conflicts raised and improves its merging capabilities. We have implemented the algorithm in Agda, a proof assistant with dependent types, and developed a model to reason about “diffing” and merging. We have formalized sanity properties and specifications of diff3 and proved that our algorithm meets them. Furthermore, we have identified the minimal conditions under which the merging algorithm raises a conflict and established a structural invariant preserved.

Nyckelord: Diff3, Dependent Types, Datatype-Generic Programming

Denna post skapades 2017-05-10.
CPL Pubid: 249246


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)


Teoretisk datalogi

Chalmers infrastruktur