Skip to main content
expanded formal definition
Source Link
Koenig Lear
  • 659
  • 6
  • 14

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

For exampleConsider the following axiomatic definition:

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

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

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

$$\forall s:string . ( \forall i \in \mathbb Z . i \geq len(s) \implies replaceAt(s,i,`x`) = s )$$$$\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 the definitionthese 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 assumptionsdifferences in the implementation models of each language.

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

For example

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

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

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

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

If you can prove the correctness of each implementation to the definition 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 assumptions in the implementation models of each language.

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.

expanded formal definition
Source Link
Koenig Lear
  • 659
  • 6
  • 14

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

For example

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

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

$$\forall s:string, \forall i \geq len(s)~.~replaceAt(s,i,`x`) = s$$$$\forall s:string . ( \forall i,j \in 0..len(s)-1 . i \neq j \implies replaceAt(s,i,`x`)[j] = s[j] )$$

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

If you can prove the correctness of each implementation to the definition 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. If you can prove the correctness of each implementation I'd say they're equivalent.

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

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

For example

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

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

$$\forall s:string, \forall i \geq len(s)~.~replaceAt(s,i,`x`) = s$$

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. If you can prove the correctness of each implementation I'd say they're equivalent.

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

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

For example

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

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

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

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

If you can prove the correctness of each implementation to the definition 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 assumptions in the implementation models of each language.

syntax correction
Source Link
Koenig Lear
  • 659
  • 6
  • 14

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

For example

$\forall s:string, i \in 0.. len(s)-1\\ \ replace(s,i,`x`)[i] = `x`$$$replaceAt: string * \mathbb Z *char \to string$$

$\forall s:string, i \geq len(s)\\ replace(s,i,`x`) = s$$$\forall s:string, \forall i \in 0.. len(s)-1~.~replaceAt(s,i,`x`)[i] = `x`$$

$$\forall s:string, \forall i \geq len(s)~.~replaceAt(s,i,`x`) = s$$

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. If you can prove the correctness of each implementation I'd say they're equivalent.

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

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

For example

$\forall s:string, i \in 0.. len(s)-1\\ \ replace(s,i,`x`)[i] = `x`$

$\forall s:string, i \geq len(s)\\ replace(s,i,`x`) = s$

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. If you can prove the correctness of each implementation I'd say they're equivalent.

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

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

For example

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

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

$$\forall s:string, \forall i \geq len(s)~.~replaceAt(s,i,`x`) = s$$

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. If you can prove the correctness of each implementation I'd say they're equivalent.

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

edited for clarity - above -> correctness
Source Link
Koenig Lear
  • 659
  • 6
  • 14
Loading
edited (function->implementation) for clarity
Source Link
Koenig Lear
  • 659
  • 6
  • 14
Loading
Source Link
Koenig Lear
  • 659
  • 6
  • 14
Loading