لغة برمجة ATS

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

في مجال الحوسبة، تُعدّ ATS ( نظام الأنواع التطبيقي ) لغة برمجة وظيفية متعددة الأنماط ، متعددة الأغراض ، وعالية المستوى . وهي لهجة من لغة البرمجة ML ، صممها هونغوي شي لتوحيد برمجة الحاسوب مع المواصفات الرسمية . تدعم ATS دمج إثبات النظريات مع البرمجة العملية من خلال استخدام أنظمة أنواع متقدمة . [ 2 ] وقد أظهرت نسخة سابقة من لعبة معايير لغات الحاسوب أن أداء ATS يُضاهي أداء لغتي C و C++ . [ 3 ] وباستخدام إثبات النظريات والتحقق الصارم من الأنواع، يستطيع المُصرّف اكتشاف وإثبات أن الدوال المُنفذة غير عُرضة للأخطاء مثل القسمة على صفر ، وتسرب الذاكرة ، وتجاوز سعة المخزن المؤقت ، وغيرها من أشكال تلف الذاكرة ، وذلك عن طريق التحقق من حسابات المؤشرات وعدّ المراجع قبل تشغيل البرنامج. أيضًا، باستخدام نظام إثبات النظريات المتكامل لـ ATS (ATS/LF)، يمكن للمبرمج الاستفادة من البنى الثابتة المتشابكة مع الكود التشغيلي لإثبات أن الدالة تتوافق مع مواصفاتها.

يتكون نظام ATS من مكون ثابت ومكون ديناميكي. يُستخدم المكون الثابت لمعالجة الأنواع، بينما يُستخدم المكون الديناميكي للبرامج. على الرغم من أن ATS يعتمد بشكل أساسي على لغة وظيفية تعتمد على استدعاء القيم، إلا أنه يتمتع بالقدرة على استيعاب نماذج برمجة متنوعة ، مثل البرمجة الوظيفية ، والبرمجة الإجرائية ، والبرمجة كائنية التوجه ، والبرمجة المتزامنة ، والبرمجة المعيارية .

تاريخ

بحسب المؤلف، استُلهمت لغة ATS من نظرية الأنواع البنائية لبير مارتن-لوف ، والتي طُوّرت في الأصل بهدف إرساء أساس للرياضيات. وقد صمّم شي لغة ATS "في محاولة لدمج المواصفات والتنفيذ في لغة برمجة واحدة". [ 4 ]

تُستمد لغة ATS في الغالب من لغتي ML و OCaml . وقد تم دمج لغة سابقة، هي Dependent ML ، من نفس المؤلف، في لغة ATS.

كُتبت النسخة الأولى، ATS/Proto (ATS0)، بلغة OCaml وصدرت عام 2006. كانت هذه النسخة بمثابة الإصدار التجريبي الأول من ATS، ولم تعد تُحدَّث. بعد عام، صدرت ATS/Geizella، وهي النسخة الأولى من ATS1. كُتبت هذه النسخة أيضًا بلغة OCaml، ولم تعد تُستخدم بشكل فعّال. [ 5 ]

شكّلت النسخة الثانية من لغة ATS1، وهي ATS/Anairiats، التي صدرت عام 2008، علامة فارقة في تطوير اللغة، إذ مكّنتها من بناء نفسها ذاتيًا. كُتبت هذه النسخة بالكامل تقريبًا بلغة ATS1. أما النسخة الحالية، ATS/Postiats (ATS2)، فقد صدرت عام 2013. ومثل سابقتها، كُتبت هذه النسخة أيضًا بالكامل تقريبًا بلغة ATS1. أحدث نسخة صدرت هي ATS2-0.4.2. [ 5 ]

مستقبل

اعتبارًا من عام 2024تُستخدم لغة ATS في الغالب لأغراض البحث؛ إذ لا يتجاوز عدد مستودعات GitHub التي تحتوي على شفرة مكتوبة بها 200 مستودع. وهذا أقل بكثير من لغات البرمجة الوظيفية الأخرى، مثل OCaml وStandard ML، اللتين تضمّان أكثر من 16000 و3000 مستودع على التوالي. يُعزى ذلك على الأرجح إلى صعوبة تعلّم ATS ، نتيجةً لاستخدامها التحقق من الأنواع التابعة وحلّ نماذج القوالب. تتطلب هذه الميزات عادةً استخدام مُحدِّدات كمية صريحة ، الأمر الذي يستلزم مزيدًا من التعلّم. [ 6 ]

اعتبارًا من عام 2024يتم تطوير ATS/Xanadu (ATS3) بنشاط في ATS2، على أمل تقليل التعلم المطلوب من خلال تحسينين رئيسيين:

يأمل شي، من خلال هذه التحسينات، أن تصبح لغة ATS أكثر سهولة في الاستخدام والتعلم. والهدف الرئيسي من ATS3 هو تحويلها من لغة تُستخدم بشكل أساسي في الأبحاث إلى لغة قوية بما يكفي لتطوير البرمجيات الصناعية واسعة النطاق. [ 5 ]

إثبات النظريات

يركز نظام ATS بشكل أساسي على دعم التحقق الرسمي من خلال إثبات النظريات الآلي ، بالتزامن مع البرمجة العملية. [ 2 ] يمكن لإثبات النظريات، على سبيل المثال، أن يثبت أن الدالة المُنفذة لا تُسبب أي تسريبات للذاكرة. كما يمكنه منع الأخطاء الأخرى التي قد لا تُكتشف إلا أثناء الاختبار. يتضمن النظام آلية مشابهة لآليات مساعدي البرهان التي تهدف عادةً إلى التحقق من البراهين الرياضية فقط، إلا أن ATS يستخدم هذه الآلية لإثبات أن تطبيقات دواله تعمل بشكل صحيح، وتُنتج المخرجات المتوقعة.

كمثال بسيط، في دالة تستخدم القسمة، يمكن للمبرمج إثبات أن المقسوم عليه لن يساوي صفرًا أبدًا، مما يمنع حدوث خطأ القسمة على صفر . لنفترض أن المقسوم عليه 'X' حُسب على أنه 5 أضعاف طول القائمة 'A'. يمكن إثبات أنه في حالة القائمة غير الفارغة، فإن 'X' لا يساوي صفرًا، لأن 'X' هو حاصل ضرب عددين غير صفريين (5 وطول 'A'). مثال عملي أكثر هو إثبات، من خلال عدّ المراجع، أن عدد مرات الاحتفاظ بكتلة ذاكرة مُخصصة يُحسب بشكل صحيح لكل مؤشر. عندها يمكن معرفة، وإثبات ذلك حرفيًا، أن الكائن لن يُحرر قبل الأوان، ولن تحدث تسريبات للذاكرة .

تكمن فائدة نظام ATS في أنه بما أن جميع عمليات إثبات النظريات تتم داخل المُصرّف فقط، فلا يؤثر ذلك على سرعة البرنامج القابل للتنفيذ. غالبًا ما يكون تجميع كود ATS أصعب من تجميع كود C القياسي ، ولكن بمجرد تجميعه، يُصبح من المؤكد أنه يعمل بشكل صحيح وفقًا للدرجة المحددة في البراهين (بافتراض صحة المُصرّف ونظام التشغيل).

في نظام ATS، تكون البراهين منفصلة عن التنفيذ، لذلك من الممكن تنفيذ دالة دون إثباتها، إذا رغب في ذلك.

تمثيل البيانات

بحسب المؤلف، تعود كفاءة لغة ATS [ 7 ] إلى حد كبير إلى طريقة تمثيل البيانات في اللغة وتحسينات استدعاءات الدوال (التي تُعدّ مهمة عمومًا لكفاءة اللغات الوظيفية). ويمكن تخزين البيانات في تمثيل مسطح أو غير مُغلّف بدلاً من التمثيل المُغلّف.

إثبات النظريات: حالة تمهيدية

الافتراضات

datapropيعبر عن المسندات كأنواع جبرية .

الشروط في الشفرة الزائفة مشابهة إلى حد ما لمصدر ATS (انظر أدناه للحصول على مصدر ATS صالح):

FACT(n, r) إذا وفقط إذا كان fact(n) = r MUL(n, m, prod) if if n * m = prod
FACT ( n , r ) = FACT ( 0 , 1 ) | FACT ( n , r ) إذا وفقط إذا كان FACT ( n - 1 , r1 ) و MUL ( n , r1 , r ) // لـ n > 0// يعبر عن fact(n) = r إذا وفقط إذا كان r = n * r1 و r1 = fact(n-1)

في كود ATS:

dataprop FACT ( int , int ) = | FACTbas ( 0 , 1 ) // الحالة الأساسية: FACT(0, 1) | { n : int | n > 0 } { r , r1 : int } // الحالة الاستقرائية FACTind ( n , r ) of ( FACT ( n - 1 , r1 ), MUL ( n , r1 , r ))

أين FACT (int, int)نوع الإثبات

مثال

مضروب غير ذيلي متكرر مع إثبات اقتراح أو " نظرية " من خلال بناء dataprop .

تُعيد عملية التقييم fact1(n-1)زوجًا (proof_n_minus_1 | result_of_n_minus_1)يُستخدم في حساب fact1(n). تُعبّر البراهين عن محمولات القضية.

الجزء الأول (الخوارزمية والافتراضات)

[ FACT ( n , r )] يستلزم [ fact ( n ) = r ] [ MUL ( n , m , prod )] يستلزم [ n * m = prod ]FACT ( 0 , 1 ) FACT ( n , r ) iff إذا وفقط إذا كان FACT ( n - 1 , r1 ) و MUL ( n , r1 , r ) لجميع n > 0

للتذكر:

{...} التحديد الكمي الشامل [...] التحديد الكمي الوجودي (... | ...) (إثبات | قيمة) @(...) صف مسطح أو صف معاملات دالة متغيرة .<...>. مقياس الإنهاء [ 8 ]
# تضمين "share/atspre_staload.hats"dataprop FACT ( int , int ) = | FACTbas ( 0 , 1 ) of () // الحالة الأساسية | { n : nat }{ r : int } // الحالة الاستقرائية FACTind ( n + 1 , ( n + 1 )* r ) of ( FACT ( n , r ))(* لاحظ أن int(x) ، وكذلك int x ، هو النوع أحادي القيمة لقيمة int x.يُشير توقيع الدالة أدناه إلى: لكل n: عدد طبيعي، يوجد r: عدد صحيح حيث fact( num: عدد صحيح(n)) تُرجع (FACT (n, r) | عدد صحيح(r)) *)دالة حقيقة { n : عدد طبيعي } .< n >. ( n : عدد صحيح ( n )) : [ r : عدد صحيح ] ( FACT ( n , r ) | int ( r )) = ( ifcase | n > 0 => (( FACTind ( pf1 ) | n * r1 )) حيث { val ( pf1 | r1 ) = fact ( n - 1 ) } | _ (*else*) => ( FACTbas () | 1 ) )

الجزء الثاني (الروتين والاختبار)

implement main0 ( argc , argv ) = { val () = if ( argc != 2 ) then prerrln ! ( "Usage: " , argv [ 0 ], " <integer>" )val () = assert ( argc >= 2 ) val n0 = g0string2int ( argv [ 1 ]) val n0 = g1ofg0 ( n0 ) val () = assert ( n0 >= 0 ) val (_ (*pf*) | res ) = fact ( n0 )val ( (*void*) ) = println ! ( "fact(" , n0 , ") = " , res ) }

يمكن إضافة كل هذا إلى ملف واحد وتجميعه كما يلي. من المفترض أن يعمل التجميع مع مختلف مُجمِّعات لغة C، مثل مجموعة مُجمِّعات GNU (gcc). لا يتم استخدام جمع البيانات المهملة-D_ATS_GCATS إلا إذا تم تحديده صراحةً باستخدام ) [ 9 ]

$ patscc Fact1.dats -o Fact1 $ ./fact1 4

يتم تجميعها وتعطي النتيجة المتوقعة

سمات

الأنواع الأساسية

  • منطقي (صواب، خطأ)
  • int (literals: 255, 0377, 0xFF), unary minus as ~ (as in ML )
  • مزدوج
  • الحرف 'أ'
  • سلسلة "abc"

الصفوف والسجلات

  • يشير البادئة @ أو لا شيء إلى تخصيص مباشر أو مسطح أو غير مُغلّف 
    val x : @( int , char ) = @( 15 , 'c' ) // x.0 = 15 ; x.1 = 'c' val @( a , b ) = x // ربط مطابقة النمط، a= 15، b='c' val x = @{ first = 15 , second = 'c' } // x.first = 15 val @{ first = a , second = b } = x // a= 15, b='c' val @{ second = b , ...} = x // مع الحذف، b='c'
  • البادئة تعني التخصيص غير المباشر أو المخصص 
    val x : ' ( int , char ) = ' ( 15 , 'c' ) // x.0 = 15 ; x.1 = 'c' val ' ( a , b ) = x // a= 15, b='c' val x = ' { first = 15 , second = 'c' } // x.first = 15 val ' { first = a , second = b } = x // a= 15, b='c' val ' { second = b , ...} = x // b='c'
  • خاص
    باستخدام |الفاصل، تُعيد بعض الدوال قيمة النتيجة مُغلّفة بتقييم المسندات
val ( predicate_proofs | values) = myfunct params

شائع

{...} التحديد الكمي الشامل [...] التحديد الكمي الوجودي (...) تعبير بين قوسين أو مجموعة (... | ...) (برهان | قيم)
.<...>. مقياس الإنهاء @(...) صف مسطح أو صف معاملات دالة متغيرة (انظر مثال printf ) @[byte][BUFLEN] نوع مصفوفة من قيم BUFLEN من النوع byte [ 10 ] مثيل مصفوفة @[byte][BUFLEN]() تمت تهيئة المصفوفة @[byte][BUFLEN](0) إلى 0

قاموس

فرز:النطاق
sortdef nat = { a : int | a >= 0 } // من prelude: ∀ a ∈ int ...typedef String = [ a : nat ] string ( a ) // [..]: ∃ a ∈ nat ...
النوع (كفرز)
فرز عام للعناصر التي يبلغ طولها طول كلمة مؤشر، لاستخدامها في الدوال متعددة الأشكال ذات المعاملات النوعية. تُعرف أيضًا باسم "الأنواع المُغلّفة" [ 11 ]
// {..}: ∀ a,b ∈ type ... fun { a , b : type } swap_type_type ( xy : @( a , b )): @( b , a ) = ( xy . 1 , xy . 0 )
يكتب
نسخة خطية من النوع السابق بطول مجرد. وكذلك الأنواع غير المعبأة. [ 11 ]
نوع العرض
نوع يشبه فئة المجال مع عرض (ارتباط بالذاكرة)
viewt@ype
نسخة خطية من نوع العرض مع طول مجرد. وهي مجموعة فرعية من نوع العرض
منظر
العلاقة بين نوع وموقع في الذاكرة. الرمز @ هو أكثر مُنشئاتها شيوعًا.
T @ Lيؤكد وجود منظر من النوع T في الموقع L
دالة { a : t @ ype } ptr_get0 { l : addr } ( pf : a @ l | p : ptr l ): @( a @ l | a )دالة { a : t @ ype } ptr_set0 { l : addr } ( pf : a ? @ l | p : ptr l , x : a ): @( a @ l | void )
نوع [ 12 ]ptr_get0 (T)​∀l:addr.(T@l|ptr(l))->(T@l|T)// see manual, section 7.1. Safe Memory Access through Pointers
viewdef array_v ( a : viewt @ ype , n : int , l : addr ) = @[ a ][ n ] @ l
ت؟
نوع غير مهيأ على الأرجح

استنفاد مطابقة الأنماط

كما في case+ , val+ , type+ , viewtype+ , ...

  • عند استخدام اللاحقة '+'، يُصدر المُترجم خطأً في حالة وجود بدائل غير شاملة.
  • بدون لاحقة، يصدر المترجم تحذيراً
  • باستخدام "-" كلاحقة، يتجنب التحكم في الشمولية

الوحدات

staload "foo.sats" // يتم تحميل foo.sats ثم فتحه في مساحة الاسم الحاليةstaload F = "foo.sats" // لاستخدام المعرفات المؤهلة كـ $F.bardynload "foo.dats" // يتم تحميلها ديناميكيًا أثناء التشغيل

عرض البيانات

غالبًا ما يتم تعريف طرق عرض البيانات لترميز العلاقات المعرفة بشكل متكرر على الموارد الخطية. [ 13 ]

dataview array_v ( a : viewt @ ype +, int , addr ) = | { l : addr } array_v_none ( a , 0 , l ) | { n : nat } { l : addr } array_v_some ( a , n + 1 , l ) of ( a @ l , array_v ( a , n , l + sizeof a ))

نوع البيانات / نوع عرض البيانات

أنواع البيانات [ 14 ]

نوع البيانات أيام العمل = الاثنين | الثلاثاء | الأربعاء | الخميس | الجمعة

القوائم

datatype list0 (a:t@ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)

نوع عرض البيانات

يُشبه نوع عرض البيانات نوع البيانات، ولكنه خطي. مع نوع عرض البيانات، يُسمح للمبرمج بتحرير (أو إلغاء تخصيص) الذاكرة المستخدمة لتخزين المُنشئات المرتبطة بنوع عرض البيانات بشكل صريح وآمن. [ 15 ]

المتغيرات

المتغيرات المحلية

var res : int with pf_res = 1 // يُعرّف pf_res كاسم بديل لـ ''view @ (res)''

حول تخصيص مصفوفة المكدس:

#define BUFLEN 10 var ! p_buf with pf_buf = @[ byte ][ BUFLEN ]( 0 ) // pf_buf = @ [ byte][BUFLEN](0) @p_buf

[ 16 ]

انظر إلى تعريفات val و var [ 17 ]

مراجع

  1. ↑ شي، هونغوي (14 نوفمبر 2020). " إصدار ATS2-0.4.2 [ ats-lang-users ] " . تم الاطلاع عليه بتاريخ 17 نوفمبر 2020 .
  2. 1 2 "دمج البرمجة مع إثبات النظريات" (ملف PDF) . مؤرشف من النسخة الأصلية (ملف PDF) بتاريخ 29-11-2014 . تم الاطلاع عليه بتاريخ 18-11-2014 .
  3. ↑ معايير ATS | لعبة معايير لغات البرمجة (أرشيف الويب)
  4. ↑ "مقدمة في البرمجة بلغة ATS" . ats-lang.github.io . تم ​​الاطلاع عليه بتاريخ 23-02-2024 .
  5. 1 2 3 "ATS-PL-SYS" . www.cs.bu.edu . تم الاطلاع عليه بتاريخ 23-02-2024 .
  6. 1 2 شي، هونغوي (2024/02/17). "githwxi/ATS-Xanadu" . جيثب . تم الاسترجاع 2024-02-23 .
  7. ↑ نقاش حول كفاءة اللغة (مقارنة اللغات: ATS هي الأفضل الآن. تتفوق على C++.)
  8. ↑ "مقاييس الإنهاء" . مؤرشف من الأصل بتاريخ 18-10-2016 . تم الاطلاع عليه بتاريخ 20-05-2017 .
  9. ↑ تجميع - مجموعة المهملات، مؤرشفة في 4 أغسطس 2009، على موقع Wayback Machine
  10. ↑ نوع من أنواع المصفوفات، مؤرشف في 4 سبتمبر 2011، في آلة Wayback Machine، أنواع مثل @[T][I]
  11. 1 2 "مقدمة في الأنواع التابعة" . مؤرشف من الأصل بتاريخ 12-03-2016 . تم الاطلاع عليه بتاريخ 13-02-2016 .
  12. ↑ الدليل، القسم 7.1. الوصول الآمن إلى الذاكرة من خلال المؤشرات (قديم)
  13. ↑ بنية عرض البيانات ( مؤرشفة في 13 أبريل 2010، على موقع Wayback Machine)
  14. ↑ بنية نوع البيانات مؤرشفة في 14 أبريل 2010 على موقع Wayback Machine
  15. ↑ بنية نوع عرض البيانات
  16. ↑ دليل المستخدم - 7.3 تخصيص الذاكرة على المكدس (مؤرشف في 9 أغسطس 2014، على موقع Wayback Machine (قديم))
  17. ↑ إعلانات Val و Var مؤرشفة في 9 أغسطس 2014، في Wayback Machine (قديمة)