¿Cómo probar que reemplazar un carácter en una cadena en C y JavaScript es equivalente?

Question

Me gustaría probar algunas pruebas diferentes, específicamente para demostrar la equivalencia de la implementación de alguna característica en dos lenguajes de programación diferentes (C y JS en esta pregunta).

Esto se trata de demostrar que que reemplaza un carácter en una cadena es equivalente en C y JS.

en JS, por ejemplo, cadenas son inmutable , mientras que en C, cadenas son mutables . Por lo tanto, en JS, es posible que tenga que hacer esto:

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

Mientras que en C podría simplemente hacer algo como esto:

#include<stdio.h>

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

Básicamente, estoy tratando de presentar un ejemplo en el que, el efecto percibido o deseado es para todos los efectos y propósitos < fuerte> lo mismo . Es decir, el resultado final es que el carácter se reemplazó a una posición específica (la misma posición en cada idioma). Aunque en un idioma, la cadena fue mutable , mientras que en el otro, fue inmutable . ¿Qué debe tenerse en cuenta aquí para hacer una prueba diciendo que estos son equivalentes? ¿Cómo captamos la noción de "equivalencia parcial" o "equivalencia percibida"? (Por eso me refiero, el resultado es aproximadamente el mismo, por lo que queremos hacer una declaración de prueba de que estos son los mismos con respecto a algunas especificaciones).

Answer 1

Empezaría creando una definición formal de la función que desea y luego demostrar para la corrección cada una de las implementaciones.

Considere la siguiente definición axiomática:

$$ reemplazo: cadena * \ mathbb z * char \ to string $$

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

$$ \ forall c: char. (\ forall s: cadena. (\ forall i \ en 0 .. len (s) -1 ~. ~ Reemplazo (s, i, c) [i]= c)) $$

$$ \ forall c: char. (\ forall s: cadena. (\ forall i \ en 0 .. len (s) -1 ~. ~ len (reemplazo (s, i, c))= len (s))) $$ < / p>

$$ \ forall c: char. (\ forall s: cadena. (\ forall i, j \ in 0..len (s) -1. I \ neq j \ implica un reemplazo (s, i, c) [j]= s [j])) $$

$$ \ forall c: char. (\ forall s: cadena. (\ forall i \ in \ mathbb z. i \ geq len (s) \ implica reemplazo (s , i, c)= s)) $$

Si puede probar la exactitud de cada implementación a estos axiomas, diría que son equivalentes. En este momento, la implementación de C no es una función. Su función JavaScript toma una cadena y no un char. Ninguno de ellos se define para índices mayores que su entrada.

No creo que la ejecución de la implementación tiene sentido, ya que hay muchas diferencias en los modelos de implementación de cada idioma.