Pendekatan teknik untuk pengembangan perangkat lunak

Bagaimana cara menguji ide, arsitektur dan algoritma tanpa menulis kode? Bagaimana cara merumuskan dan memverifikasi propertinya? Apa itu pemeriksa model dan pencari model? Persyaratan dan spesifikasi - peninggalan masa lalu?

Hai Nama saya Vasil Dyadov, sekarang saya bekerja sebagai programmer di Yandex, sebelum itu saya bekerja di Intel, saya dulu mengembangkan kode RTL (register transfer level) pada Verilog / VHDL untuk ASIC / FPGA. Saya telah lama menyukai topik keandalan perangkat lunak dan perangkat keras, matematika, alat, dan metode yang digunakan untuk mengembangkan perangkat lunak dan logika dengan properti yang telah ditentukan sebelumnya.

Ini adalah artikel pertama saya dalam seri yang dirancang untuk menarik perhatian pengembang dan manajer pada pendekatan teknik untuk pengembangan perangkat lunak. Baru-baru ini, ia telah diabaikan dengan tidak patut, meskipun ada perubahan revolusioner dalam pendekatan dan alat pendukungnya.

Saya tidak akan menyembunyikan: tugas utama artikel ini adalah untuk membangkitkan minat. Jadi akan ada minimum penalaran yang panjang dan maksimum spesifisitas.

Artikel ini memiliki dua bagian. Pada bagian pertama saya akan menjelaskan apa yang saya maksud dengan pendekatan teknik, pada bagian kedua saya akan menunjukkan contoh penggunaan pendekatan dalam kerangka tugas sederhana (dekat dengan bidang arsitektur layanan mikro).

Saya selalu terbuka untuk membahas masalah yang terkait dengan pengembangan perangkat lunak, dan saya akan senang mengobrol dengan pembaca (koordinat untuk komunikasi ada di profil saya).

Bagian 1. Pendekatan teknik untuk pengembangan

Apa ini Saya akan menunjukkan kepada Anda contoh membangun jembatan:

• Tahap 1 adalah pengumpulan persyaratan untuk jembatan: jenis jembatan, kapasitas muat, dll.
• Tahap 2 - spesifikasi persyaratan dan perhitungan struktur (spesifikasi).
• Tahap 3 - konstruksi aktual itu sendiri berdasarkan perhitungan teknik (spesifikasi).

Tentu saja, ini analogi yang disederhanakan. Tidak ada yang membuat jembatan prototipe untuk menjelaskan persyaratan dan spesifikasi. Parameterisasi tidak dapat ditambahkan ke jembatan sehingga menjadi melengkung atau ditangguhkan. Tapi secara keseluruhan, saya pikir analoginya jelas.

Dalam pengembangan perangkat lunak, langkah 1 dan 2 sering tidak ada atau sangat lemah diekspresikan. Jika persyaratannya ditetapkan, maka tidak jelas, tidak lengkap, dan informal. Hanya beberapa persyaratan detail dan kembangkan spesifikasi yang jelas.

Banyak orang berpikir bahwa ini adalah buang-buang waktu, peninggalan masa lalu, terutama jika pendekatan tangkas untuk pembangunan dipilih (terutama dengan iterasi singkat). Dan ini adalah kesalahan besar.

Mengapa

Untuk mulai dengan, kita akan memahami apa persyaratan dan spesifikasi seperti itu dan apa perbedaan signifikan mereka, yang tidak selalu jelas bagi banyak profesional.

Apa saja persyaratannya?

Singkatnya, persyaratan adalah perumusan properti produk dalam hal area subjek. Misalnya, seperti ini: "Semua instance dari program harus sama memproses permintaan input."

Persyaratan tidak menggunakan ketentuan ruang lingkup implementasi. Begitu istilah "sinkronisasi negara", Raft, Paxos, "kompleksitas logaritmik dalam waktu" bocor ke dalam persyaratan, maka persyaratan dan spesifikasi mulai bercampur.

Penting untuk memahami hal ini dan dengan jelas memisahkan satu dari yang lain.

Mengapa

1. Persyaratan harus jelas bagi konsumen perangkat lunak, oleh karena itu, mereka harus berasal dari bidang subjek yang sedang dikembangkan perangkat lunak (seringkali, para ahli yang jauh dari pengembangan harus dilibatkan dalam merumuskan persyaratan dan menetapkan tugas untuk pengembangan perangkat lunak).

   
   

2. Properti perangkat lunak yang dilihat konsumen dievaluasi oleh metrik area subjek. Penting untuk memisahkan persyaratan dan spesifikasi agar dapat 1) mengidentifikasi metrik produk utama yang digunakan konsumen untuk mengevaluasi perangkat lunak kami, dan 2) memahami dengan jelas properti produk mana yang penting bagi pengguna dan mana yang tidak.

   
   

Kalau tidak, itu bisa berubah seperti ini: pengembang, tidak memenuhi tenggat waktu, akan mengorbankan properti penting dan mencurahkan banyak waktu dan perhatian untuk yang tidak penting. Selain itu, apa yang tampaknya penting dari sudut pandang pengembangan perangkat lunak mungkin tidak penting dari sudut pandang pengguna.

Contoh klasik dari perbedaan tersebut diberikan dalam berbagai literatur tentang pengembangan antarmuka pengguna dan dalam artikel (misalnya: Waktu Respons Sistem dan Kepuasan Pengguna: Studi Eksperimental Aplikasi Berbasis Browser , Latensi Komputer: 1977-2017 ). Pengembang biasanya mencoba untuk mengoptimalkan waktu pelaksanaan operasi, misalnya, mencari informasi dalam database, dan waktu respons pengguna adalah penting. Dan jika pencarian lambat, tetapi pengguna mulai melihat hasil yang dikembalikan secepat mungkin, maka menurutnya perangkat lunak tersebut berfungsi lebih baik daripada yang pencarian dengan cepat, tetapi pertama-tama mengakumulasi hasil dan akhirnya menampilkan semuanya.

Itulah sebabnya perencana sumber daya OS berbeda untuk mode operasi server dan desktop. Untuk mode server, throughput maksimum sistem adalah penting, mis., Optimalisasi waktu dan memori untuk menggunakan server secara efisien. Dan bagi pengguna, keterlambatan dalam respons sistem adalah penting. Semakin cepat sistem merespons tindakan, semakin cepat tampaknya, bahkan jika kerjanya lebih lambat.

Dan akhirnya, alasan terpenting:

Jika persyaratan dan spesifikasi tercampur, itu artinya kita tidak sepenuhnya memahami tugas-tugas yang sedang kita kembangkan perangkat lunak. Kami mulai merumuskan dan menyelesaikan masalah dari bidang subjek di bidang pengembangan perangkat lunak. Karenanya, logika domain bocor dan membingungkan logika kode. Hasilnya adalah kode yang digabungkan secara ketat yang sulit untuk dipertahankan.

Ini ditulis dengan baik oleh Michael Jackson dalam buku Problem Frames: Analyzing & Structure Problem Development Software . Menurut pendapat saya, ini adalah salah satu buku paling berguna untuk pengembang perangkat lunak. Pertama-tama ia mengajarkan untuk menganalisis masalah pengguna, yang harus dipecahkan oleh perangkat lunak yang baik. Program supercepat yang menghabiskan sedikit sumber daya sistem tetapi tidak menyelesaikan tugas pengguna adalah program yang buruk. Keren tapi jelek.

Apa spesifikasinya?

Spesifikasi adalah perumusan properti perangkat lunak dalam hal bidang pengembangan perangkat lunak. Di sinilah konsep kompleksitas, sinkronisasi, dll.

Spesifikasi dapat diatur secara hierarkis: dari abstrak ke spesifik, di mana Anda dapat menulis kode. Pendekatan ini seringkali paling efektif. Spesifikasi abstrak dengan mudah mencerminkan arsitektur - Anda dapat melihat properti dasar, menemukan kesalahan arsitektur, dll. Oleh karena itu, kami dapat menemukan masalah pada tahap awal siklus hidup perangkat lunak dan secara signifikan mengurangi biaya perbaikan kesalahan.

Penting untuk diperhatikan manfaat dan pentingnya spesifikasi untuk protokol dan antarmuka antara komponen sistem, yang akan membantu menghindari situasi ini:

Apa perbedaan dari pendekatan pengembangan yang biasa?

Dalam pendekatan teknik, kami melakukan pra-desain perangkat lunak dengan karakteristik yang diperlukan sesuai dengan spesifikasi. Kami memeriksa spesifikasi untuk properti yang diperlukan yang berasal dari persyaratan.

Saya membuat perbandingan dalam bentuk tablet (sangat subyektif):

Dan bukankah model agitasi untuk model pengembangan air terjun di sini?

Rekayasa perangkat lunak, termasuk spesifikasi dan simulasi formal, berjalan dengan baik dengan pendekatan gesit.

Diyakini bahwa pendekatan rekayasa untuk pengembangan tidak sesuai dengan pengembangan perangkat lunak berulang yang cepat (seperti yang dinyatakan dalam banyak artikel, berikut adalah contohnya ).

Tapi ini tidak benar. Pendekatan teknik telah berhasil diterapkan di banyak proyek, termasuk proyek dengan iterasi pendek.

Sebelumnya, karena sarana dan alat pendukung yang kurang berkembang, pendekatan teknik memang terkait erat dengan model air terjun.

Tetapi sekarang semuanya telah berubah secara dramatis.

Berkat keberhasilan terobosan dalam bidang pemodelan, pemecah SAT / SMT, dll., Sekarang memungkinkan untuk dengan cepat memeriksa ruang besar status sistem untuk mengetahui properti yang kita butuhkan dan tidak adanya yang tidak perlu, untuk memverifikasi volume industri kode, dll.

Alat industri kelas satu seperti Alloy, TLA + / TLC, Atelier B, PRISM muncul, yang mengalihkan tugas memformalkan dan memeriksa spesifikasi dari bidang akademik / matematika, yang membutuhkan kualifikasi tinggi dan upaya besar, ke tugas tombol, dapat diakses oleh sebagian besar programmer.

Spesifikasi sekarang dapat dikembangkan secara iteratif dan bertahap. Model dirancang dengan baik secara iteratif, dari abstrak hingga beton. Waktu simulasi bahkan untuk sistem besar dihitung dalam hitungan menit dan jam.

Persyaratan mudah ditentukan secara iteratif, terutama dengan pendekatan dan alat modern.
Dan penyempurnaan persyaratan, spesifikasi, refactoring model, penulisan kode dan refactoringnya dapat dengan mudah berjalan paralel - dalam satu iterasi.

Secara umum, pendekatan teknik sekarang sama sekali tidak sama dengan model air terjun, ini adalah dua hal yang independen.

Pendekatan teknik mudah dikombinasikan dengan metodologi pengembangan organisasi.

Blog Hillel Wayne menunjukkan betapa mudahnya bekerja dengan spesifikasi dan model formal. Dia memiliki contoh yang bagus tentang bagaimana secara formal menentukan logika antarmuka pengguna suatu program dalam 10 menit dan memeriksa beberapa propertinya.

Saya tidak akan masuk ke detail dan menerjemahkan seluruh artikel, saya hanya akan menunjukkan spesifikasi itu sendiri di Alloy :

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
   .