Engineering-Ansatz für die Softwareentwicklung

Wie kann man Ideen, Architekturen und Algorithmen testen, ohne Code zu schreiben? Wie formuliere und verifiziere ich ihre Eigenschaften? Was sind Modellprüfer und Modellfinder? Anforderungen und Spezifikationen - ein Relikt der Vergangenheit?

Hallo. Mein Name ist Vasil Dyadov, jetzt arbeite ich als Programmierer in Yandex. Bevor ich bei Intel arbeitete, entwickelte ich RTL-Code (Register Transfer Level) auf Verilog / VHDL für ASIC / FPGA. Ich habe mich lange mit dem Thema Software- und Hardware-Zuverlässigkeit, Mathematik, Tools und Methoden beschäftigt, die zur Entwicklung von Software und Logik mit garantierten, vordefinierten Eigenschaften verwendet werden.

Dies ist mein erster Artikel in einer Reihe, die Entwickler und Manager auf den technischen Ansatz für die Softwareentwicklung aufmerksam machen soll. In letzter Zeit wurde er trotz revolutionärer Änderungen in seinem Ansatz und seinen Unterstützungsinstrumenten zu Unrecht ignoriert.

Ich werde nicht zerstreuen: Die Hauptaufgabe des Artikels ist es, Interesse zu wecken. Es wird also ein Minimum an langwierigen Überlegungen und ein Maximum an Spezifität geben.

Der Artikel besteht aus zwei Teilen. Im ersten werde ich beschreiben, was ich unter dem Engineering-Ansatz verstehe, im zweiten ein Beispiel für die Verwendung des Ansatzes im Rahmen einer einfachen Aufgabe (in der Nähe des Bereichs der Microservice-Architektur).

Ich bin immer offen für Fragen im Zusammenhang mit der Softwareentwicklung und freue mich, mit den Lesern zu chatten (die Koordinaten für die Kommunikation finden Sie in meinem Profil).

Teil 1. Engineering-Ansatz für die Entwicklung

Was ist das? Ich zeige Ihnen das Beispiel eines Brückenbaus:

• Stufe 1 ist die Erfassung der Anforderungen an die Brücke: Brückentyp, Tragfähigkeit usw.
• Stufe 2 - Spezifikation der Anforderungen und Berechnung der Strukturen (Spezifikation).
• Stufe 3 - die eigentliche Konstruktion selbst basierend auf technischen Berechnungen (Spezifikationen).

Dies ist natürlich eine vereinfachte Analogie. Niemand stellt Prototypenbrücken her, um Anforderungen und Spezifikationen zu klären. Die Bridge kann nicht parametrisiert werden, sodass sie entweder gewölbt oder angehalten wird. Aber insgesamt denke ich, dass die Analogie klar ist.

In der Softwareentwicklung fehlen die Schritte 1 und 2 häufig oder werden nur sehr schwach ausgedrückt. Wenn die Anforderungen festgelegt sind, sind sie vage, unvollständig und informell. Nur wenige Detailanforderungen und klare Spezifikationen entwickeln.

Viele Leute halten dies für Zeitverschwendung, ein Relikt der Vergangenheit, insbesondere wenn der agile Entwicklungsansatz gewählt wird (insbesondere bei kurzen Iterationen). Und das ist ein großer Fehler.

Warum?

Zunächst werden wir verstehen, was eine solche Anforderung und Spezifikation ist und was ihr wesentlicher Unterschied ist, der für viele Fachleute nicht immer offensichtlich ist.

Was sind die Anforderungen?

Kurz gesagt, Anforderungen sind die Formulierung von Produkteigenschaften in Bezug auf den Themenbereich. Beispiel: "Alle Instanzen des Programms sollten Eingabeanforderungen gleichermaßen verarbeiten."

Die Anforderungen verwenden nicht die Bedingungen des Umsetzungsumfangs. Sobald die Begriffe "Zustandssynchronisation", Floß, Paxos, "logarithmische Komplexität in der Zeit" in die Anforderungen eingehen, beginnen sich die Anforderungen und Spezifikationen zu vermischen.

Es ist wichtig, dies zu verstehen und klar voneinander zu trennen.

Warum?

1. Die Anforderungen sollten den Verbrauchern von Software klar sein, daher sollten sie aus dem Themenbereich stammen, für den Software entwickelt wird (häufig müssen Experten, die weit von der Entwicklung entfernt sind, in die Formulierung von Anforderungen und die Festlegung einer Aufgabe für die Softwareentwicklung einbezogen werden).

   
   

2. Software-Eigenschaften, die ein Verbraucher sieht, werden anhand von Themenbereichsmetriken bewertet. Es ist notwendig, Anforderungen und Spezifikationen zu trennen, um 1) die wichtigsten Produktmetriken identifizieren zu können, anhand derer der Verbraucher unsere Software bewertet, und 2) klar zu verstehen, welche Produkteigenschaften für den Benutzer wichtig sind und welche nicht.

   
   

Andernfalls könnte sich Folgendes herausstellen: Entwickler, die die Frist nicht einhalten, werden wichtige Eigenschaften opfern und unwichtigen viel Zeit und Aufmerksamkeit widmen. Darüber hinaus ist das, was aus Sicht der Softwareentwicklung wichtig erscheint, aus Sicht des Benutzers möglicherweise nicht wichtig.

Ein klassisches Beispiel für eine solche Diskrepanz findet sich in einer Vielzahl von Literatur zur Entwicklung von Benutzeroberflächen und in Artikeln (zum Beispiel: Systemantwortzeit und Benutzerzufriedenheit: Eine experimentelle Studie zu browserbasierten Anwendungen , Computerlatenz: 1977–2017 ). Entwickler versuchen normalerweise, die Ausführungszeit eines Vorgangs zu optimieren, z. B. indem sie nach Informationen in einer Datenbank suchen. Die Antwortzeit des Benutzers ist wichtig. Und wenn die Suche langsam ist, der Benutzer jedoch die zurückgegebenen Ergebnisse so schnell wie möglich sieht, scheint ihm eine solche Software besser zu funktionieren als die, die schnell sucht, aber zuerst die Ergebnisse sammelt und schließlich alle anzeigt.

Aus diesem Grund unterscheiden sich die Ressourcenplaner des Betriebssystems in den Betriebsarten Server und Desktop. Für den Servermodus ist der maximale Durchsatz des Systems wichtig, d. H. Die Optimierung von Zeit und Speicher, um den Server effizient zu nutzen. Für den Benutzer ist die Verzögerung der Reaktion des Systems wichtig. Je schneller das System auf Aktionen reagiert, desto schneller scheint es, auch wenn es langsamer arbeitet.

Und schließlich der wichtigste Grund:

Wenn Anforderungen und Spezifikationen gemischt sind, bedeutet dies, dass wir die Aufgaben, für die wir Software entwickeln, nicht vollständig verstehen. Wir beginnen Probleme aus dem Fachgebiet der Softwareentwicklung zu formulieren und zu lösen. Daher tritt die Domänenlogik aus und verwirrt die Codelogik. Das Ergebnis ist eng gekoppelter Code, der schwer zu pflegen ist.

Dies wurde von Michael Jackson in dem Buch Problem Frames: Analysieren und Strukturieren von Softwareentwicklungsproblemen gut geschrieben. Meiner Meinung nach ist dies eines der nützlichsten Bücher für Softwareentwickler. Es lehrt zunächst, die Probleme der Benutzer zu analysieren, die eine gute Software lösen sollte. Ein superschnelles Programm, das wenig Systemressourcen verbraucht, aber keine Benutzeraufgaben löst, ist ein schlechtes Programm. Cool aber schlecht.

Was ist die Spezifikation?

Eine Spezifikation ist eine Formulierung von Softwareeigenschaften in Bezug auf ein Softwareentwicklungsfeld. Hier liegen die Konzepte von Komplexität, Synchronisation usw.

Spezifikationen können hierarchisch organisiert werden: von abstrakt bis spezifisch, auf die Sie Code schreiben können. Dieser Ansatz ist oft der effektivste. Abstrakte Spezifikationen spiegeln leicht die Architektur wider - Sie können die grundlegenden Eigenschaften sehen, Architekturfehler finden usw. Daher können wir Probleme in den frühen Phasen des Software-Lebenszyklus finden und die Kosten für die Behebung von Fehlern erheblich senken.

Es ist besonders erwähnenswert, welchen Nutzen und welche Bedeutung Spezifikationen für Protokolle und Schnittstellen zwischen Systemkomponenten haben, um diese Situationen zu vermeiden:

Was ist der Unterschied zum üblichen Entwicklungsansatz?

Im Engineering-Ansatz entwerfen wir Software mit den erforderlichen Eigenschaften gemäß den Spezifikationen vor. Wir überprüfen die Spezifikationen für die erforderlichen Eigenschaften, die sich aus den Anforderungen ergeben.

Ich habe einen Vergleich in Form einer Tablette gemacht (sehr subjektiv):

Und ist hier nicht das Agitationsmodell für ein Wasserfallentwicklungsmodell?

Software-Engineering, einschließlich formaler Spezifikationen und Simulationen, passt gut zum agilen Ansatz.

Es wird angenommen, dass der technische Entwicklungsansatz nicht mit der schnellen iterativen Softwareentwicklung kompatibel ist (wie in vielen Artikeln angegeben, hier ein Beispiel ).

Aber das ist nicht so. Der Engineering-Ansatz wurde erfolgreich in vielen Projekten angewendet, einschließlich Projekten mit kurzen Iterationen.

Zuvor war der technische Ansatz aufgrund schlecht entwickelter Mittel und Hilfsmittel tatsächlich eng mit dem Wasserfallmodell verbunden.

Aber jetzt hat sich alles dramatisch verändert.

Dank bahnbrechender Erfolge auf dem Gebiet der Modellierung, SAT / SMT-Löser usw. ist es jetzt möglich, große Bereiche von Systemzuständen schnell auf das Vorhandensein der benötigten und das Fehlen unnötiger Eigenschaften zu überprüfen, um industrielle Codemengen usw. zu überprüfen.

Es erschienen erstklassige industrielle Werkzeuge wie Alloy, TLA + / TLC, Atelier B, PRISM, die die Aufgabe der Formalisierung und Überprüfung von Spezifikationen von akademisch / mathematisch, die hohe Qualifikationen und enormen Aufwand erfordern, auf die Druckknopfaufgabe übertragen, die den meisten Programmierern zugänglich ist.

Spezifikationen können jetzt iterativ und inkrementell entwickelt werden. Modelle sind iterativ gut gestaltet, von abstrakt bis konkret. Die Simulationszeit auch großer Systeme wird in Minuten und Stunden berechnet.

Die Anforderungen lassen sich leicht iterativ festlegen, insbesondere bei modernen Ansätzen und Tools.
Die Verfeinerung von Anforderungen, Spezifikationen, das Refactoring von Modellen, das Schreiben von Code und das Refactoring können problemlos parallel erfolgen - innerhalb einer Iteration.

Im Allgemeinen entspricht der technische Ansatz jetzt überhaupt nicht mehr dem Wasserfallmodell, dies sind zwei unabhängige Dinge.

Der Engineering-Ansatz lässt sich leicht mit jeder Methodik der Entwicklungsorganisation kombinieren.

Hillel Waynes Blog zeigt, wie einfach es ist, mit formalen Spezifikationen und Modellen zu arbeiten. Er hat ein großartiges Beispiel dafür, wie man die Logik der Benutzeroberfläche eines Programms in 10 Minuten formal spezifiziert und einige seiner Eigenschaften überprüft.

Ich werde nicht auf Details eingehen und den gesamten Artikel übersetzen, sondern nur die Spezifikation selbst in Alloy zeigen :

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
   .