Como provar que substituir um caractere em uma string tanto em C quanto em JavaScript é equivalente?

Question

Gostaria de tentar algumas provas diferentes, especificamente para provar a equivalência da implementação de algum recurso em duas linguagens de programação diferentes (C e JS nesta questão).

Trata-se de provar que substituindo um caractere em uma string é equivalente em C e JS.

Em JS, por exemplo, cordas são imutável, enquanto em C, cordas são mutável.Então, em JS você pode ter que fazer isso:

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

Enquanto estiver em C, você pode fazer algo assim:

#include<stdio.h>

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

Basicamente, estou tentando encontrar um exemplo onde, o efeito percebido ou resultado desejado é para todos os efeitos o mesmo.Ou seja, o resultado final é que o caractere foi substituído em uma posição específica (a mesma posição em cada idioma).Mesmo que em um idioma a string fosse mutável, enquanto no outro foi imutável.O que precisa ser levado em conta aqui para fazer uma prova dizendo que estes são equivalentes?Como captamos a noção de “equivalência parcial” ou “equivalência percebida”?(Com isso quero dizer que o resultado é praticamente o mesmo, então queremos fazer uma prova de que são iguais em relação a algumas especificações).

Answer 1

Eu começaria criando uma definição formal da função que você deseja e depois provaria a correção de cada uma das implementações.

Considere a seguinte definição axiomática:

$$substituirEm:string * \mathbb Z *char o 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 eq j \implica substituirAt(s,i,c)[j] = s[j] ))$$

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

Se você puder provar a exatidão de cada implementação desses axiomas, eu diria que eles são equivalentes.No momento seu C implementação nem é uma função.Seu JavaScript função recebe uma string e não um caractere.Nenhum deles está definido para índices maiores que a sua entrada.

Não acho que comparar implementação com implementação faça sentido, pois há muitas diferenças nos modelos de implementação de cada linguagem.