Goodbye C developers: The future of programming with certified program synthesis

It just so happens that this same reasoning procedure presented above for synthesising swap actually scales quite well, and can be directly used to verify more complex programs like list copy.

To illustrate how well this works let's have a look at the process of synthesising the base case of list copy from before:

// r :-> x ** linked_list(x,S)
void listcopy(void **r) {
  ???
}
// r :-> y ** linked_list(y,S) ** linked_list(x,S)

Following the same reasoning as before, the synthesis starts by emitting a read operation:

void listcopy(void **r) {
  void *x2 = *r;
// r :-> x2 ** linked_list(x2,S)
  ???
}
// r :-> y ** linked_list(y,S) ** linked_list(x2,S)

In order to proceed further, the synthesis must unfold the definition of the heap predicate for linked lists, and this naturally translates into an if-else-statement for each case of the predicate:

void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    // r :-> x2 ** emp; x2 == NULL && S = {}
    ???
    // r :-> y ** linked_list(y,S) ** linked_list(x2,S)
  } ...
}

For the base-case, the synthesis procedure can propagate the equalities, x2 == NULL and S = {}, that the constructor exposes across both the pre and post-condition without having to emit any new statements:

void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    // r :-> NULL ** emp
    ???
    // r :-> y ** linked_list(y,{}) ** linked_list(NULL,{})
  } ...
}

At this point, the synthesis procedure notices that the linked_list(y,{}) predicate can be satisfied by instantiating y with NULL:

void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    // r :-> NULL ** emp
    ???
    // r :-> NULL ** emp
  } ...
}

At this point, the pre and post-conditions are equal, and so the synthesis procedure knows that it has successfully synthesised the base case of the function:

// r :-> x ** linked_list(x,S)
void listcopy(void **r) {
  void *x2 = *r;
  if (x2 == NULL) {
    return;
  } ...
}
// r :-> y ** linked_list(y,S) ** linked_list(x,S)

A similar search procedure can be done on the inductive case as well, and eventually leads to the original code presented in the introduction. The SuSLik paper also demonstrates this technique can be used to synthesise a variety of other complex algorithms, such as tree flattening, sorting, binary search trees etc.

from Hacker News https://ift.tt/3wiHnKW