ما هو "رسمي دلالات"?

Question

أنا أقرأ جدا سخيفة الورق ويبقى في الحديث عن كيف جيوتو يعرف "الرسمية دلالات".

جيوتو الرسمي دلالات الذي يحدد معنى وضع مفاتيح, من intertask الاتصال و التواصل مع برنامج البيئة.

أنا على حافة ، ولكن فقط لا يمكن فهم تماما ما يعنيه "الرسمية دلالات."

Answer 1

الدلالات الرسمية صف الدلالات في - حسناً ، طريقة رسمية - باستخدام تدوين يعبر عن معنى الأشياء بطريقة لا لبس فيها.

إنه عكس غير رسمي الدلالات ، والتي هي في الأساس مجرد وصف كل شيء باللغة الإنجليزية العادي. قد يكون هذا أسهل في القراءة والفهم ، لكنه يخلق إمكانية تفسير سوء التفسير ، مما قد يؤدي إلى الأخطاء لأن شخصًا ما لم يقرأ فقرة بالطريقة التي تنوي قراءتها.

يمكن أن تحتوي لغة البرمجة على دلالات رسمية وغير رسمية - ستكون الدلالات غير الرسمية بمثابة شرح "نص عادي" للدلالات الرسمية ، وستكون الدلالات الرسمية هي المكان المناسب للبحث إذا لم تكن متأكدًا من التفسير غير الرسمي حقا يعني.

Answer 2

للتوسع في إجابة مايكل مادسن قليلاً ، قد يكون مثال على سلوك مشغل ++. بشكل غير رسمي ، نصف المشغل باستخدام اللغة الإنجليزية العادية. على سبيل المثال:

لو x هو متغير من النوع int, ++x أسباب x لزيادة واحد.

(أفترض عدم وجود أي فلاط عدد صحيح ، وذاك ++x لا يعيد أي شيء)

في دلالات رسمية (وسأستخدم الدلالات التشغيلية) ، سيكون لدينا القليل من العمل. أولاً ، نحتاج إلى تحديد فكرة الأنواع. في هذه الحالة ، سأفترض أن جميع المتغيرات من النوع int. في هذه اللغة البسيطة ، يمكن وصف الحالة الحالية للبرنامج بواسطة متجر ، وهو رسم خرائط من المتغيرات إلى القيم. على سبيل المثال ، في مرحلة ما من البرنامج ، x قد يكون مساويا 42 ، بينما y يساوي -5351. يمكن استخدام المتجر كدالة - لذلك ، على سبيل المثال ، إذا كان المتجر s لديه المتغير x مع القيمة 42 ، ثم s(x) = 42.

كما تم تضمينها في الوضع الحالي للبرنامج هي البيانات المتبقية للبرنامج الذي يتعين علينا تنفيذه. يمكننا تجميع هذا الأمر <C, s>, ، أين C هو البرنامج المتبقي ، و s هو المتجر.

لذلك ، إذا كان لدينا الدولة <++x, {x -> 42, y -> -5351}>, ، هذه حالة غير رسمية حيث يكون الأمر المتبقي الوحيد الذي يجب تنفيذه ++x, ، المتغير x لديه قيمة 42 ، والمتغير y له قيمة -5351.

يمكننا بعد ذلك تحديد التحولات من حالة من البرنامج إلى آخر - نصف ما يحدث عندما نتخذ الخطوة التالية في البرنامج. وذلك ل ++, ، يمكننا تحديد الدلالات التالية:

<++x, s> --> <skip, s{x -> (s(x) + 1)>

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

<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}>

نأمل أن يمنحك هذا الفكرة. لاحظ أن هذا مجرد مثال واحد على الدلالات الرسمية - إلى جانب الدلالات التشغيلية ، هناك دلالات بديهية (والتي تستخدم في كثير من الأحيان منطق Hoare) ودلالات الدلالة ، وربما أكثر من ذلك لا أعرفها.

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

Answer 3

تماما مثل بناء جملة لغة يمكن وصفها رسمي النحوي (مثلا ، BNF) ، فمن الممكن استخدام أنواع مختلفة من الشكليات إلى خريطة الجملة الرياضية الكائنات (أيمعنى الجملة).

هذه الصفحة من مقدمة عملية إلى Denotational دلالات هو مقدمة لطيفة كيف [denotational] دلالات تتعلق الجملة.بداية الكتاب كما يعطي لمحة تاريخية أخرى غير denotational النهج الرسمي دلالات (على الرغم من ويكيبيديا الرابط مايكل أعطى يذهب إلى المزيد من التفاصيل, و ربما أكثر ما يصل إلى تاريخ).

من موقع البلاغ:

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

Answer 4

ما هو المقصود في سياق لغة البرمجة مثل Giotto ، أن لغة ذات دلالات رسمية ، لديها أ صارمة رياضيا تفسير بنيات لغته الفردية.

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

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

من ناحية أخرى ، يتم تعريف C أو C ++ بشكل غير رسمي بواسطة الأوصاف الفنية ، على الرغم من وجود أوراق أكاديمية تضفي جوانب هذه اللغات (على سبيل المثال ، Michael Norrish: دلالات رسمية لـ C ++ ، https://publications.csiro.au/rpr/pub؟pid=nicta:1203) ، لكن في كثير من الأحيان لا يجد طريقهم إلى المعايير الرسمية (ربما بسبب عدم وجود التطبيق العملي ، صعوبة في الحفاظ عليها).