How to prove that replacing a character in a string in both C and JavaScript is equivalent?

Question

I would like to try some different proofs, specifically in proving equivalence of the implementation of some feature in two different programming languages (C and JS in this question).

This is about proving that replacing one character in a string is equivalent in C and JS.

In JS, for example, strings are immutable, while in C, strings are mutable. So in JS you might have to do this:

functioni replaceAt(string, index, replacement) {
  return string.substr(0, index) + replacement + string.substr(index + replacement.length)
}

While in C you might just do something like this:

#include<stdio.h>

int
main() {
  char string[11] = "hello world";
  string[1] = 'i';
  printf("%s", string);
  return 0;
}

Basically, I am trying to come up with an example where, the perceived effect or desired outcome is for all intents and purposes the same. That is, the end result is that the character was replaced at a specific position (the same position in each language). Even though in one language the string was mutable, while in the other, it was immutable. What needs to be taken into account here to make a proof saying these are equivalent? How do we capture the notion of "partial equivalence" or "perceived equivalence"? (By that I mean, the outcome is roughly the same, so we want to make a proof statement that these are the same with regard to some spec).

Answer 1

I would start by creating a formal definition of the function that you want and then proving for correctness each of the implementations.

Consider the following axiomatic definition:

$$replaceAt: string * \mathbb Z *char \to string$$

$$\forall c:char . ( \forall i \in \mathbb Z~.~replaceAt(``,i,c) = `` )$$

$$\forall c:char . (\forall s:string . ( \forall i \in 0.. len(s)-1~.~replaceAt(s,i,c)[i] = c ))$$

$$\forall c:char . (\forall s:string . ( \forall i \in 0.. len(s)-1~.~len(replaceAt(s,i,c)) = len(s) ))$$

$$\forall c:char .(\forall s:string . ( \forall i,j \in 0..len(s)-1 . i \neq j \implies replaceAt(s,i,c)[j] = s[j] ))$$

$$\forall c:char .(\forall s:string . ( \forall i \in \mathbb Z . i \geq len(s) \implies replaceAt(s,i,c) = s ))$$

If you can prove the correctness of each implementation to these axioms I'd say they're equivalent. At the moment your C implementation is not even a function. Your Javascript function takes a string and not a char. None of them are defined for indexes greater than your input.

I don't think comparing implementation to implementation makes sense as there are lot of differences in the implementation models of each language.