كيف تثبت أن استبدال حرف في سلسلة في كل من C وJavaScript متكافئ؟

Question

أرغب في تجربة بعض البراهين المختلفة، وتحديدًا في إثبات تكافؤ تنفيذ بعض الميزات في لغتين برمجة مختلفتين (C وJS في هذا السؤال).

هذا يتعلق بإثبات ذلك استبدال حرف واحد في سلسلة يعادل في C وJS.

في JS، على سبيل المثال، السلاسل هي غير قابل للتغيير, ، بينما في C، السلاسل هي متقلب.لذلك في JS قد يتعين عليك القيام بذلك:

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

أثناء وجودك في لغة C، يمكنك القيام بشيء مثل هذا:

#include<stdio.h>

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

في الأساس، أحاول التوصل إلى مثال حيث، التأثير المدرك أو النتيجة المرجوة يكون لكل النوايا و الأهداف نفس الشيء.أي أن النتيجة النهائية هي استبدال الحرف في موضع محدد (نفس الموضع في كل لغة).على الرغم من أن السلسلة كانت في لغة واحدة متقلب, ، بينما كان في الآخر غير قابل للتغيير.ما الذي يجب أخذه في الاعتبار هنا لتقديم دليل على أنهما متساويان؟كيف يمكننا التقاط فكرة "التكافؤ الجزئي" أو "التكافؤ المتصور"؟(وبهذا أعني أن النتيجة هي نفسها تقريبًا، لذلك نريد تقديم بيان إثبات على أن هذه هي نفسها فيما يتعلق ببعض المواصفات).

Answer 1

سأبدأ بإنشاء تعريف رسمي للوظيفة التي تريدها ثم إثبات صحة كل تطبيق.

النظر في التعريف البديهي التالي:

$$ استبدال في:سلسلة * \mathbb Z *char o string$$

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

$$\forall c:char .(\forall s:string .( \لجميع \في 0..len(s)-1~.~replaceAt(s,i,c)[i] = c ))$$

$$\forall c:char .(\forall s:string .( \لجميع \في 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 \يتضمن استبدالAt(s,i,c)[j] = s[j] ))$$

$$\forall c:char .(\forall s:string .( \forall i \in \mathbb Z .i \geq len(s) \يتضمن استبدالAt(s,i,c) = s ))$$

إذا كان بإمكانك إثبات صحة كل تطبيق لهذه البديهيات، فسأقول إنها متكافئة.في هذه اللحظة الخاص بك ج التنفيذ ليس حتى وظيفة.لك جافا سكريبت تأخذ الدالة سلسلة وليس حرفًا.لم يتم تعريف أي منها لفهارس أكبر من مدخلاتك.

لا أعتقد أن مقارنة التنفيذ بالتنفيذ أمر منطقي نظرًا لوجود اختلافات كثيرة في نماذج التنفيذ لكل لغة.