لغة البرمجة F*

📅 آخر تحديث: ٢٤ يوليو ٢٠٢٦
✍️ نُشر في: ٢٤ يوليو ٢٠٢٦
الموسوعة الحرة

F* (تُنطق إف ستار ) هي لغة برمجة عالية المستوى ، متعددة الأنماط ، وظيفية ، وموجهة للكائنات، مستوحاة من لغات ML و Caml و OCaml ، ومخصصة للتحقق من البرامج . وهي مشروع مشترك بين مايكروسوفت للأبحاث والمعهد الفرنسي لأبحاث علوم الحاسوب والأتمتة (Inria). [ 1 ] يتضمن نظام أنواعها أنواعًا تابعة ، وتأثيرات أحادية ، وأنواع تحسين . وهذا يسمح بالتعبير عن مواصفات دقيقة للبرامج، بما في ذلك صحة الوظائف وخصائص الأمان. يهدف مدقق أنواع F* إلى إثبات أن البرامج تفي بمواصفاتها باستخدام مزيج من حل قابلية الإرضاء المعياري للنظريات (SMT) والبراهين اليدوية . للتنفيذ، يمكن ترجمة البرامج المكتوبة بلغة F* إلى OCaml أو F# أو C أو WebAssembly (عبر أداة KaRaMeL) أو لغة التجميع (عبر مجموعة أدوات Vale). كما كان من الممكن ترجمة الإصدارات السابقة من F* إلى JavaScript .

تم طرحه في عام 2011 [ 3 ] [ 4 ] وهو قيد التطوير النشط على GitHub . [ 2 ]

تاريخ

الإصدارات

حتى الإصدار 2022.03.24، كُتبت لغة F* بالكامل باستخدام مجموعة فرعية مشتركة من F* و F# ، وكانت تدعم التمهيد في كلٍ من OCaml وF#. وقد أُلغي هذا الدعم بدءًا من الإصدار 2022.04.02. [ 5 ] [ 6 ]

ملخص

المشغلون

يدعم F* عوامل التشغيل الحسابية الشائعة مثل +، -، *، و /. كما يدعم F* عوامل التشغيل العلائقية مثل <، <=، ==، !=، >و >=. [ 7 ]

أنواع البيانات

أنواع البيانات الأولية الشائعة في F* هي bool، int، float، char، و unit. [ 7 ]

مراجع

  1. 1 2 "مركز أبحاث مايكروسوفت في إنريا المشترك" . MSR-INRIA .
  2. 1 2 "FStarLang/FStar" . GitHub . مؤرشف من الأصل في 26 أبريل 2026. تم الاسترجاع في 26 أبريل 2026 .
  3. ↑ سوامي، نيخيل؛ تشين، خوان؛ فورنيه، سيدريك؛ ستروب، بيير-إيف؛ بهارجافان، كارتيكيان؛ يانغ، جان (سبتمبر 2011). البرمجة الموزعة الآمنة باستخدام أنواع تعتمد على القيمة . ICFP '11: وقائع المؤتمر الدولي السادس عشر لـ ACM SIGPLAN حول البرمجة الوظيفية. المجلد 46. طوكيو، اليابان: رابطة آلات الحوسبة. الصفحات 266-278 . doi : 10.1145/2034574.2034811 . تاريخ الاسترجاع: 17 أبريل 2023 .  
  4. ↑ "مشروع F*" . مايكروسوفت . تم الاطلاع عليه بتاريخ 20 أبريل 2023 .
  5. ↑ "لم يعد بالإمكان إنشاء ملف fstar.exe باستخدام لغة F# كملف تنفيذي لـ .NET #2512" . جيت هاب . تم الاطلاع عليه بتاريخ 17 أبريل 2023 .
  6. ↑ "النظر في إلغاء شرط أن يكون كود F* صالحًا بلغة F# #1737" . جيت هاب . تم الاطلاع عليه في 17 أبريل 2023 .
  7. 1 2 سوامي، نيخيل؛ مارتينيز، غيدو؛ راستوجي، أسيم (14 يناير 2024). البرمجة الموجهة بالبرهان في F* (ملف PDF) .

مصادر

  • أهمن، دانيل؛ هريتكو، كاتالين؛ مايلارد، كينجي؛ مارتينيز، غيدو؛ بلوتكين، غوردون؛ بروتزينكو، جوناثان؛ راستوجي، أسيم؛ سوامي، نيخيل (2017). "مونادات ديكسترا مجانًا" . المؤتمر الرابع والأربعون لجمعية ACM SIGPLAN-SIGACT حول مبادئ لغات البرمجة .
  • سوامي، نيخيل. هريتاكو، كاتالين؛ كيلر، شانتال؛ راستوجي، عاصم؛ ديلينات لافود، أنطوان؛ فورست، سيمون؛ بهارجافان، كارثيكيان؛ فورنيه، سيدريك؛ ستروب، بيير إيف؛ كولويس، ماركولف. زينزيندوهوي، جان كريم؛ زانيلا بيجولين، سانتياغو (2016). "الأنواع التابعة والتأثيرات المتعددة الأحادية في F *" . ندوة ACM SIGPLAN-SIGACT الثالثة والأربعون حول مبادئ لغات البرمجة .
  • سوامي، نيخيل؛ مارتينيز، غيدو؛ راستوجي، أسيم (2024). البرمجة الموجهة بالبرهان في F* .