النهج الهندسي لتطوير البرمجيات

كيفية اختبار الأفكار والهندسة المعمارية والخوارزميات دون كتابة التعليمات البرمجية؟ كيفية صياغة والتحقق من ممتلكاتهم؟ ما هي لعبة الداما والباحثين عن النماذج؟ المتطلبات والمواصفات - بقايا الماضي؟

مرحبا. اسمي Vasil Dyadov ، والآن أعمل كمبرمج في Yandex ، وقبل ذلك عملت في Intel ، اعتدت على تطوير رمز RTL (مستوى نقل التسجيل) على Verilog / VHDL لـ ASIC / FPGA. لقد كنت مغرمًا منذ فترة طويلة بموضوع موثوقية البرامج والأجهزة والرياضيات والأدوات والأساليب المستخدمة لتطوير البرامج والمنطق بخصائص مضمونة ومحددة مسبقًا.

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

لن أتفكك: المهمة الرئيسية للمقال هي إثارة الاهتمام. لذلك سيكون هناك حد أدنى من المنطق الطويل والحد الأقصى من الخصوصية.

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

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

الجزء 1. النهج الهندسي للتنمية

ما هذا سأريكم مثال بناء الجسر:

• المرحلة 1 هي مجموعة متطلبات الجسر: نوع الجسر ، سعة الحمولة ، إلخ.
• المرحلة 2 - تحديد المتطلبات وحساب الهياكل (المواصفات).
• المرحلة 3 - البناء الفعلي نفسه على أساس الحسابات الهندسية (المواصفات).

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

في تطوير البرمجيات ، غالبًا ما تكون الخطوتين 1 و 2 غائبتين أو يتم التعبير عنها بشكل ضعيف جدًا. إذا تم إصلاح المتطلبات ، فهي غامضة وغير مكتملة وغير رسمية. متطلبات قليلة فقط من التفاصيل وتطوير مواصفات واضحة.

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

لماذا؟

بادئ ذي بدء ، سوف نفهم ما هو هذا الشرط والمواصفات وما هو الفرق الكبير بينهما ، وهذا ليس واضحا دائما للعديد من المهنيين.

ما هي المتطلبات؟

باختصار ، المتطلبات هي صياغة خصائص المنتج من حيث مجال الموضوع. على سبيل المثال ، مثل هذا: "يجب على جميع مثيلات البرنامج معالجة طلبات الإدخال بالتساوي."

المتطلبات لا تستخدم شروط نطاق التنفيذ. بمجرد أن تتسرب المصطلحات "تزامن الحالة" ، الطوافة ، Paxos ، "التعقيد اللوغاريتمي في الوقت المناسب" إلى المتطلبات ، ثم تبدأ المتطلبات والمواصفات في الاختلاط.

من المهم أن نفهم هذا ونفصل بوضوح عن الآخر.

لماذا؟

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

   
   

2. يتم تقييم خصائص البرنامج التي يراها المستهلك حسب مقاييس مجال الموضوع. من الضروري فصل المتطلبات والمواصفات من أجل أن تكون قادرًا على: 1) تحديد مقاييس المنتج الرئيسية التي سيقيم بها المستهلك برنامجنا ، و 2) فهم خصائص المنتج المهمة للمستخدم والتي ليست كذلك.

   
   

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

ويرد مثال كلاسيكي لمثل هذا التناقض في مجموعة متنوعة من الأدبيات المتعلقة بتطوير واجهة المستخدم وفي المقالات (على سبيل المثال: وقت استجابة النظام ورضا المستخدم: دراسة تجريبية للتطبيقات المستندة إلى المستعرض ، زمن انتقال الكمبيوتر: 1977–2017 ). عادة ما يحاول المطورون تحسين وقت تنفيذ العملية ، على سبيل المثال ، البحث عن المعلومات في قاعدة بيانات ، ووقت استجابة المستخدم مهم. وإذا كان البحث بطيئًا ، لكن المستخدم يبدأ في رؤية النتائج التي تم إرجاعها بأسرع ما يمكن ، يبدو له أن مثل هذا البرنامج يعمل بشكل أفضل من الذي يبحث بسرعة ، ولكنه أولاً يجمع النتائج ويعرضها جميعًا.

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

وأخيرا ، السبب الأكثر أهمية:

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

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

ما هي المواصفات؟

المواصفات عبارة عن صياغة لخصائص البرنامج من حيث مجال تطوير البرمجيات. هذا هو المكان الذي مفاهيم التعقيد ، التزامن ، الخ

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

تجدر الإشارة بشكل خاص إلى فائدة وأهمية مواصفات البروتوكولات والواجهات بين مكونات النظام ، مما سيساعد على تجنب هذه الحالات:

ما هو الفرق من نهج التنمية المعتادة؟

في النهج الهندسي ، نقوم بتصميم البرامج مسبقًا بالخصائص المطلوبة وفقًا للمواصفات. نحن نتحقق من مواصفات الخصائص الضرورية التي تأتي من المتطلبات.

قمت بإجراء مقارنة على شكل جهاز لوحي (ذاتي للغاية):

أليس هذا نموذج التحريض لنموذج تطوير الشلال هنا؟

هندسة البرمجيات ، بما في ذلك المواصفات والمحاكاة الرسمية ، تسير بشكل جيد مع النهج الرشيق.

يُعتقد أن النهج الهندسي للتطوير لا يتوافق مع التطوير البرمجي التكراري السريع (كما هو مذكور في العديد من المقالات ، فيما يلي مثال ).

لكن هذا ليس كذلك. تم تطبيق النهج الهندسي بنجاح في العديد من المشاريع ، بما في ذلك المشاريع ذات التكرار القصير.

في السابق ، نظرًا لضعف الوسائل وأدوات الدعم ، كان النهج الهندسي مرتبطًا ارتباطًا وثيقًا بنموذج الشلال.

ولكن الآن تغير كل شيء بشكل كبير.

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

ظهرت أدوات صناعية من الدرجة الأولى مثل Alloy و TLA + / TLC و Atelier B و PRISM ، والتي نقلت مهمة إضفاء الطابع الرسمي على المواصفات والتحقق منها من الأكاديمية / الرياضية ، والتي تتطلب مؤهلات عالية وجهود ضخمة ، إلى مهمة الضغط على زر ، في متناول معظم المبرمجين.

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

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

بشكل عام ، فإن النهج الهندسي الآن لا يساوي على الإطلاق نموذج الشلال ، فهذان شيئان مستقلان.

يتم دمج النهج الهندسي بسهولة مع أي منهجية منظمة التطوير.

تُظهر مدونة Hillel Wayne مدى سهولة العمل مع المواصفات والنماذج الرسمية. لديه مثال رائع على كيفية تحديد منطق واجهة المستخدم الخاصة بالبرنامج في غضون 10 دقائق والتحقق من بعض خصائصه.

لن أخوض في التفاصيل وأترجم المقالة بأكملها ، سأعرض المواصفات نفسها في السبائك :

open util/ordering[Time]
sig Time {
    state: one State
}
abstract sig State {}
abstract sig Login extends State {}
abstract sig Reports extends Login {}

one sig Logout extends State {}
one sig Students, Summary, Standards extends Reports {}
one sig Answers extends Login {}

pred transition[t: Time, start: State, end: State] {
  t.state in start
  t.next.state in end
}

pred logout[t: Time] { transition[t, Login, Logout] }
pred login[t: Time] { transition[t, Logout, Summary] }
pred students[t: Time] { transition[t, Reports, Students] }
pred summary[t: Time] { transition[t, Reports, Summary] }
pred standards[t: Time] { transition[t, Reports, Standards] }
pred answers[t: Time] { transition[t, Students, Answers] }
pred close_answers[t: Time] { transition[t, Answers, Students] }

fact Trace {
  first.state = Summary
  all t: Time - last |
    logout[t] or
    login[t] or
    students[t] or
    summary[t] or
    standards[t] or
    answers[t] or
    close_answers[t]
}

, . , UI .

:

check {all t: Time | t.state = Answers implies 
        t.prev.state = Students} for 7

.

, , .

agile.

— .

, , — Alloy, .

, , ( ) .

( ) , .

, .

2. Alloy

Alloy, : , , .

, — , , - .

.

, , .

$$, $$ $$.

Alloy : X->Y.

( util/relation):

module relation

-- :
-- set A -    A,   
-- one A -       A
-- lone A -    A   
-- some A -      A

-- :
-- univ -       ,
--            
-- iden -   {A0, A0},     
--               univ
--        iden = {a : univ, b: univ |  a=b}
--            
-- none -  

-- :
-- : and, or, => (), != ( ), not
--  :
-- & - 
-- A->B -      .
--        
-- X<:Y -     Y ,   
--           X
-- A in B -  A   B
-- ~A -     A
-- A + B - 
-- no A - A ,  A = none
-- ^A -     A,
--         B , :
--      A in B,
--      {E0, E1}, {E1, E2} in B => {E0, E2} in B
-- A.B -  JOIN,  . :
--       {A0, B0} in A, {B0, C0, D0} in B, 
--       {A0, C0, D0} in A.B 

-- :
-- all X : Y | .... - 
-- some X : Y | .... - 

--  :
-- pred[a: A, b:B] {...}    
-- : pred[a, b]  a.pred[b]
--       
-- -,    
-- method(self : Object, args ...)

pred valid [rel : univ->univ, dom : set univ, cod : set univ] {
  rel.univ in dom and rel.univ in cod
}
fun domain [rel : univ->univ] : set (rel.univ) { rel.univ }
fun codomain [rel : univ->univ] : set (univ.rel) { univ.rel }
pred total  [rel: univ->univ, dom: set univ] {
  all x: dom | some x.rel
}
pred partial [rel: univ->univ, dom: set univ] {
  all x: dom | lone x.rel
}
pred functional [rel: univ->univ, dom: set univ] {
  all x: dom | one x.rel
}
pred surjective [rel: univ->univ, cod: set univ] {
  all x: cod | some rel.x
}
pred injective [rel: univ->univ, cod: set univ] {
  all x: cod | lone rel.x
}
pred bijective [rel: univ->univ, cod: set univ] {
  all x: cod | one rel.x
}
pred bijection [rel: univ->univ, dom, cod: set univ] {
  rel.functional[dom] and rel.bijective[cod]
}
pred reflexive [rel: univ->univ, s: set univ] {
  s<:iden in rel
}
pred irreflexive [rel: univ->univ] {no iden & rel}
pred symmetric [rel: univ->univ] {~rel in rel}
pred antisymmetric [rel: univ->univ] {~rel & rel in iden}
pred transitive [rel: univ->univ] {rel.rel in rel}
pred acyclic [rel: univ->univ, s: set univ] {
  all x: s | x not in x.^rel
}
pred complete[rel: univ->univ, s: univ] {
  all x,y:s | (x!=y => x->y in (rel + ~rel))
}
pred preorder [rel: univ->univ, s: set univ] {
  rel.reflexive[s] and rel.transitive
}
pred equality [rel: univ->univ, s: set univ] {
  rel.preorder[s] and rel.symmetric
}
pred partial_order [rel: univ->univ, s: set univ] {
  rel.preorder[s] and rel.antisymmetric
}
pred total_order [rel: univ->univ, s: set univ] {
  rel.partial_order[s] and rel.complete[s]
}

, , Alloy.

.

utils/graph, , , :

module graph[node]
open relation

--     
fun nodes[r: node->node]: set node {
  r.domain+ r.codomain
}

--  ,     
--       
--   
pred connected[r: node->node] {
  all n1,n2 : r.nodes | n1 in n2.*(r + ~r)
}

--    
pred dag [r: node->node] {
  r.acyclic[r.nodes]
}

--    
--   ,   
--   
fun roots [r: node->node] : set node {
  let ns = r.nodes | -- ns -   
    ns - ns.^r --     ,
               --    -
               --  
}

--   
--  -  ,  
--   
fun leaves [r: node->node] : set node {
  let ns = r.nodes | -- ns -   
    ns - ns.^~r --     ,
                --    -
                --  
}

— , .

:

• (1) — , , ;
• (2) — , , ;
• (3) — , ;
• (4) , — ;
• (5) . . , , , ;
• (6) , — , .

.

, , Alloy:

module compgraph[node]

open graph[node]
open relation

pred valid [edges: node->node,
            source : one node, --  1
            drain : one node --  2
] {
  edges.antisymmetric and edges.irreflexive --  6
  graph/roots[edges] = source --  1  4
  graph/leaves[edges] = drain --  2  4
}

:

open compgraph[node] as cg -- cg -  

enum node {n0, n1, n2, n3, n4}
--    ,    

run cg/valid --     cg,  
  --  valid    : relation  compgraph

:

, ( ).

, .

, .

. . , .

, . :

• — , . . ;
• — ;
• — , . . , .

, , . . ( , ).

, :

• (7) ( ). , , ;
• (8) , . . .

, .

, , , .

• (9) , .

(, , ) :

• (10) .

:

module compgraph[node]

open graph[node]

pred active[edges : node->node,
            source: node,
            n : node
] {
  -- n    ,
  --   
  n in source.^edges
}

pred safe[edges : node->node,
          drain : node,
          n : node
] {
  --    ,  drain,
  --      n
  --      
  --  n     
  --  
  no n.*edges & (leaves[edges] - drain)
  --     , 
  --       
  --     ,
  --  ,     drain
  drain in n.*edges
}

pred valid [edges: node->node,
            source : one node, --  1
            drain : one  node --  2
] {
  edges.connected --     
                  --     ( 
                  --        ),
                  --      , 
                  -- ,   
                  --  connected
  edges.dag --  6  8
  source in edges.roots --  1, 4  9
  drain in edges.leaves --  2, 4  8
  all n : edges.roots - source |
    not active[edges, source, n] --  9
  all n : edges.nodes | -- 10 
    active[edges, source, n] => safe[edges, drain, n]
}

.

.

, .

:

1. ;
2. ;
3. ;
4. ;
5. ;
6. .

. . : .

, ? ?

.

, , .

, .

, :

• ( , );
• ;
• ;
• .

.

, .

:

1. -> ;
2. -> ;
3. -> ;
4. -> .

, .

, : , . - , — , / .

, : -> .

, :

• ;
• .

, .

, Alloy , . , Alloy .

pred connect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node, 
  to : one node
] {
  --    
  from->to not in old_edges

  -- from   to,
  --    
  from not in to.*old_edges

  -- to    ,
  --    
  -- 
  to in (old_edges.nodes - source)

  --   to  
  -- ,   
  --   to  
  safe[old_edges, drain, to]

  --    ,
  --      
  --  
  new_edges = old_edges + from->to
}

connect .

, connect :

open compgraph[node] as cg

sig node {}

check {
  --      r1, r2
  all r1, r2 : node->node |
  --     source, drain, from, to
  all source, drain, from, to : node  {
    -- r1     
    -- source/drain /
    --  r2   r1   
    -- connect  from->to
    (cg/valid[r1, source, drain] and
     connect[r1, r2, source, drain, from, to])
    --   ,  r2 + source/drain
    --    
    -- 
    implies cg/valid[r2, source, drain]
    --    connect  
    --  
  }
} for 8

Executing "Check check$1 for 8"
   Sig this/node scope <= 8
   Sig this/node in [[node$0], [node$1], [node$2], [node$3],
     [node$4], [node$5], [node$6], [node$7]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   8374 vars. 168 primary vars. 22725 clauses. 108ms.
   No counterexample found. Assertion may be valid. 26904ms

Alloy . , "168 primary vars" , $$ . 30 !

, connect .

, :

pred disconnect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node,
  to : one node
] {
  --     
  from->to in old_edges

  --    from
  --   
  safe[new_edges, drain, from]

  --    
  new_edges.connected

  --  
  new_edges = old_edges - from->to
}

:

open compgraph[node] as cg
sig node {}
check {
  all r1, r2 : node->node |
  all source, drain, from, to : node  {
    (cg/valid[r1, source, drain] and
     disconnect[r1, r2, source, drain, from, to])
    implies cg/valid[r2, source, drain]
  }
} for 8

! ! :

disconnect:

pred disconnect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node,
  to : one node
] {
  from->to in old_edges
  ( safe[new_edges, drain, from] or
   (from not in new_edges.nodes and
    from != source))
  new_edges.connected
  new_edges = old_edges - from >to
}

Executing "Check check$2 for 8"
   Sig this/node scope <= 8
   Sig this/node in [[node$0], [node$1], [node$2], [node$3], [node$4], [node$5], [node$6], [node$7]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   8505 vars. 168 primary vars. 24808 clauses. 207ms.
   No counterexample found. Assertion may be valid. 18369ms.

, .

, ?

, ? ?

:

--     
--     ,
-- ,       
--       
check {
  all r1,r2: node->node | all source,drain: node |
  some intermediate : seq node->node {
     cg/valid[r1, source, drain] and cg/valid[r2, source, drain]
     =>
     intermediate.first = r1 and
     intermediate.last = r2 and
     all i : intermediate.inds - intermediate.lastIdx {
       let from = intermediate[i] |
       let to = intermediate[i+1] |
       some n1, n2 : node |
         connect[from,to, source, drain, n1, n2]
         or
         disconnect[from, to, source, drain, n1, n2]
     }
  }
} for 3

:

Executing "Check check$3"
   Sig this/node scope <= 3
   Sig this/node in [[node$0], [node$1], [node$2]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
A type error has occured: (see the stacktrace)
Analysis cannot be performed since it requires higher-order
quantification that could not be skolemized.

?

Alloy: .

«some intermediate…», — .

.

( , ) , .

higher-order Alloy, , . , CEGIS — counter-example guided inductive synthesis.

, .

, , , :

check {
  all edges, edges1 : node->node |
  all source,drain, from, to : node {
    (cg/valid[edges, source, drain] and
    cg/valid[edges1, source, drain] and
    edges1 = edges + from->to and
    edges1 != edges)
    =>
    some n1, n2: node | connect[edges, edges1, source, drain, n1, n2]
  }
} for 7

, :

Executing "Check check$3 for 7"
   Sig this/node scope <= 7
   Sig this/node in [[node$0], [node$1], [node$2], [node$3],
     [node$4], [node$5], [node$6]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   6471 vars. 133 primary vars. 16634 clauses. 200ms.
   Counterexample found. Assertion is invalid. 116ms.

!

connect:

pred connect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node, 
  to : one node
] {
  from->to not in old_edges
  from not in to.*old_edges
  to in (old_edges.nodes - source)
  --   
  active[old_edges, source, from] => safe[old_edges, drain, to]
  --   to    from,
  -- ,   to     ,
  --   from,    
  --   
  new_edges.connected
  --   ,    
  --    :)
  new_edges = old_edges + from -> to
}

:

Executing "Check check$3 for 7"
   Sig this/node scope <= 7
   Sig this/node in [[node$0], [node$1], [node$2], [node$3],
     [node$4], [node$5], [node$6]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
   6513 vars. 133 primary vars. 16837 clauses. 125ms.
   No counterexample found. Assertion may be valid. 291ms.

.

disconnect. , :

pred disconnect[
  old_edges : node->node,
  new_edges : node->node,
  source : one node,
  drain : one node,
  from : one node,
  to : one node
] {
  from->to in old_edges
  --       ,
  --     
  active[old_edges, source, from] => safe[new_edges, drain, from]
  -- ,      
  -- ,     :
  -- (from not in new_edges.nodes and
  --  from != source)

  new_edges.connected
  new_edges = old_edges - from->to
}

, , / , .

, , (, source->drain), connect/disconnect .

( , , ).

?

, .

, , , . .

: , ( safe/active .).

.

, .

, — , . .

, .

, .

, , ( ) .

?

Alloy .

.

, , , Python.

, ( ) .

?

Alloy Analyzer, GitHub — .

Alloy?

:

• , , - ;
• , , , assert’ , . .;
• ( );
• , , , . , , .

. Facebook, Google, Microsoft, Amazon .

• Amazon Web Services, , (Use of Formal Methods at Amazon Web Services, Formal reasoning about the security of Amazon Web Services, Amazon Relies on Formal Methods for the Security of AWS)
• Facebook ().
• Google ().
• Microsoft , (Spec#, Formal Methods at Scale in Microsoft, Formal Methods and Toolsfor Distributed Systems).

, , .

agile- , .

, : .

.

.

, , , , (TLA+/TLC, B-method/Atelier B, Promela/SPIN). .

, , , . .

1. Michael Jackson Problem Frames: Analysing & Structuring Software Development Problems
   ( !), . , .
2. Daniel Jackson Software Abstractions: Logic, Language, and Analysis
   model finder Alloy . , . ( join, ). , .
3. . MODEL CHECKING.
   . , , . , .

Alloy

1. Pamela Zave. How to Make Chord Correct
   Alloy DHT Chord, ( , ), . , .
   
   1. 
      Alloy, .

1. Hillel Wayne
   . , . , .

1. . . , . . , . . .
   , , .

Alloy

1. Alloy Analyzer + Higher-Order Alloy
   Alloy.
2. Online Tutorial
   , .
3. Tutorial Materials
   .