Skip to content

Latest commit

 

History

History
28 lines (20 loc) · 4.82 KB

README.md

File metadata and controls

28 lines (20 loc) · 4.82 KB

Correct-by-construction refactoring of functional code

Agda

This repository contains a correct-by-construction approach for refactoring tuples to records in a Haskell-like language (HLL). This is done for the 2022/2023 edition of the BSc Research Project at the Delft Univesity of Technology. An example of the refactoring operation is shown below.

-- Before
lastName :: (String, String, Int) -> String
lastName (_, s, _) = s

-- After
data Person = Person { initials :: String
                     , lastName :: String
                     , age :: Int
                     }

Folder structure

All relevant information can be found in the src folder. The structure is as follows:

  • HLL - Intrinsically-typed specification of the HLL and big-step semantics.
  • Proofs - Proof that the refactoring operation replaces all tuples by record instances and a relation between values of a pre-refactored and refactored expression.
  • Refactoring - Refactoring operation that replaces all tuples by record instances. Treats all tuples as if they were unique. The accompanying record declaration is based on the type signature of the tuple.
  • Utils - Utility folder that contains a construct which specifies that some element is in a list.