Approche d'ingénierie pour le développement de logiciels

Comment tester des idées, l'architecture et les algorithmes sans écrire de code? Comment formuler et vérifier leurs propriétés? Que sont les vérificateurs de modèles et les chercheurs de modèles? Exigences et spécifications - une relique du passé?

Salut Je m'appelle Vasil Dyadov, maintenant je travaille comme programmeur chez Yandex, avant de travailler chez Intel, je développais du code RTL (niveau de transfert de registre) sur Verilog / VHDL pour ASIC / FPGA. Je m'intéresse depuis longtemps au sujet de la fiabilité des logiciels et du matériel, des mathématiques, des outils et des méthodes utilisés pour développer des logiciels et de la logique avec des propriétés prédéfinies garanties.

Ceci est mon premier article d'une série conçue pour attirer l'attention des développeurs et des gestionnaires sur l'approche d'ingénierie du développement logiciel. Récemment, il a été indûment ignoré, malgré des changements révolutionnaires dans son approche et ses outils de soutien.

Je ne vais pas dissimuler: la tâche principale de l'article est de susciter l'intérêt. Il y aura donc un minimum de raisonnement long et un maximum de spécificité.

L'article comporte deux parties. Dans la première je décrirai ce que j'entends par approche d'ingénierie, dans la seconde je montrerai un exemple d'utilisation de l'approche dans le cadre d'une tâche simple (proche du domaine de l'architecture de microservices).

Je suis toujours ouvert pour discuter des questions liées au développement de logiciels, et je serai heureux de discuter avec les lecteurs (les coordonnées de communication sont dans mon profil).

Partie 1. Approche technique du développement

Qu'est ce que c'est Je vais vous montrer l'exemple de la construction d'un pont:

• L'étape 1 est la collecte des exigences pour le pont: le type de pont, la capacité de charge, etc.
• Étape 2 - spécification des exigences et calcul des structures (spécification).
• Étape 3 - la construction proprement dite basée sur des calculs d'ingénierie (spécifications).

Bien sûr, il s'agit d'une analogie simplifiée. Personne ne crée de ponts prototypes pour clarifier les exigences et les spécifications. Le paramétrage ne peut pas être ajouté au pont afin qu'il devienne soit arqué soit suspendu. Mais dans l'ensemble, je pense que l'analogie est claire.

En développement logiciel, les étapes 1 et 2 sont souvent absentes ou très faiblement exprimées. Si les exigences sont fixes, elles sont vagues, incomplètes et informelles. Seulement quelques exigences détaillées et des spécifications claires.

Beaucoup de gens pensent que c'est une perte de temps, une relique du passé, surtout si l'approche agile du développement est choisie (surtout avec de courtes itérations). Et c'est une grosse erreur.

Pourquoi?

Pour commencer, nous comprendrons ce qu'est une telle exigence et spécification et quelle est leur différence significative, ce qui n'est pas toujours évident pour de nombreux professionnels.

Quelles sont les exigences?

En bref, les exigences sont la formulation des propriétés du produit en termes de domaine. Par exemple, comme ceci: "Toutes les instances du programme doivent traiter également les demandes d'entrée."

Les exigences n'utilisent pas les termes du champ d'application. Dès que les termes «synchronisation d'état», Raft, Paxos, «complexité logarithmique dans le temps» fuient dans les exigences, les exigences et les spécifications commencent à se mélanger.

Il est important de comprendre cela et de bien séparer les uns des autres.

Pourquoi?

1. Les exigences doivent être claires pour les consommateurs de logiciels, par conséquent, elles doivent être du domaine pour lequel le logiciel est développé (souvent, des experts qui sont loin du développement doivent être impliqués dans la formulation des exigences et la définition d'une tâche pour le développement de logiciels).

   
   

2. Les propriétés logicielles qu'un consommateur voit sont évaluées par des mesures de domaine. Il est nécessaire de séparer les exigences et les spécifications afin de pouvoir 1) identifier les principales mesures du produit par lesquelles le consommateur évaluera notre logiciel, et 2) comprendre clairement quelles propriétés du produit sont importantes pour l'utilisateur et lesquelles ne le sont pas.

   
   

Sinon, cela peut se produire comme ceci: les développeurs, ne respectant pas la date limite, sacrifieront des propriétés importantes et consacreront beaucoup de temps et d'attention à des propriétés sans importance. De plus, ce qui semble important du point de vue du développement logiciel peut ne pas l'être du point de vue de l'utilisateur.

Un exemple classique d'une telle divergence est donné dans une variété de littérature sur le développement d'interfaces utilisateur et dans des articles (par exemple: System Response Time and User Satisfaction: An Experimental Study of Browser-based Applications , Computer latency: 1977-2017 ). Les développeurs tentent généralement d'optimiser le temps d'exécution d'une opération, par exemple, en recherchant des informations dans une base de données, et le temps de réponse de l'utilisateur est important. Et si la recherche est lente, mais que l'utilisateur commence à voir les résultats retournés le plus rapidement possible, il lui semble que ce logiciel fonctionne mieux que celui qui recherche rapidement, mais accumule d'abord les résultats et les affiche finalement tous.

C'est pourquoi les planificateurs de ressources OS diffèrent pour les modes de fonctionnement serveur et bureau. Pour le mode serveur, le débit maximal du système est important, c'est-à-dire l'optimisation du temps et de la mémoire afin d'utiliser efficacement le serveur. Et pour l'utilisateur, le retard dans la réponse du système est important. Plus le système réagit rapidement aux actions, plus il semble rapide, même s'il fonctionne plus lentement.

Et enfin, la raison la plus importante:

Si les exigences et les spécifications sont mélangées, cela signifie que nous ne comprenons pas pleinement les tâches pour lesquelles nous développons des logiciels. Nous commençons à formuler et à résoudre des problèmes du domaine dans le domaine du développement logiciel. Par conséquent, la logique du domaine fuit et confond la logique du code. Le résultat est un code étroitement couplé qui est difficile à maintenir.

Cela a été bien écrit par Michael Jackson dans le livre Problem Frames: Analyzing & Structuring Software Development Problems . À mon avis, c'est l'un des livres les plus utiles pour les développeurs de logiciels. Il apprend tout d'abord à analyser les problèmes des utilisateurs, qu'un bon logiciel devrait résoudre. Un programme ultra-rapide qui consomme peu de ressources système mais ne résout pas les tâches utilisateur est un mauvais programme. Cool mais mauvais.

Quelle est la spécification?

Une spécification est une formulation de propriétés logicielles en termes de domaine de développement logiciel. C'est là que les concepts de complexité, de synchronisation, etc.

Les spécifications peuvent être organisées de manière hiérarchique: du résumé au spécifique, sur lequel vous pouvez écrire du code. Cette approche est souvent la plus efficace. Les spécifications abstraites reflètent facilement l'architecture - vous pouvez voir les propriétés de base, trouver des erreurs architecturales, etc. Par conséquent, nous pouvons trouver des problèmes dans les premières étapes du cycle de vie du logiciel et réduire considérablement le coût de la correction des erreurs.

Il convient en particulier de noter les avantages et l'importance des spécifications pour les protocoles et les interfaces entre les composants du système, qui aideront à éviter ces situations:

Quelle est la différence avec l'approche de développement habituelle?

Dans la démarche d'ingénierie, nous pré-concevons un logiciel avec les caractéristiques requises conformément au cahier des charges. Nous vérifions les spécifications pour les propriétés nécessaires qui proviennent des exigences.

J'ai fait une comparaison sous forme de tablette (très subjective):

Et n'est-ce pas le modèle d'agitation d'un modèle de développement en cascade ici?

L'ingénierie logicielle, y compris même les spécifications formelles et les simulations, va bien avec l'approche agile.

On pense que l'approche d'ingénierie du développement est incompatible avec un développement logiciel itératif rapide (comme indiqué dans de nombreux articles, voici un exemple ).

Mais ce n'est pas le cas. L'approche d'ingénierie a été appliquée avec succès dans de nombreux projets, y compris des projets avec de courtes itérations.

Auparavant, en raison de moyens et d'outils d'appui peu développés, la démarche d'ingénierie était en effet étroitement liée au modèle de la cascade.

Mais maintenant, tout a radicalement changé.

Grâce à des succès décisifs dans le domaine de la modélisation, des solveurs SAT / SMT, etc., il est désormais possible de vérifier rapidement de vastes espaces d'états de système pour la présence des propriétés dont nous avons besoin et l'absence de propriétés inutiles, pour vérifier les volumes industriels du code, etc.

Des outils industriels de première classe tels que Alloy, TLA + / TLC, Atelier B, PRISM sont apparus, qui ont transféré la tâche de formalisation et de vérification des spécifications de l'enseignement / mathématiques, nécessitant des qualifications élevées et des efforts considérables, à la tâche de bouton-poussoir, accessible à la plupart des programmeurs.

Les spécifications peuvent désormais être développées de manière itérative et incrémentielle. Les modèles sont bien conçus de manière itérative, de l'abstrait au béton. Le temps de simulation même de grands systèmes est calculé en minutes et en heures.

Les exigences sont faciles à spécifier de manière itérative, en particulier avec les approches et outils modernes.
Et le raffinement des exigences, des spécifications, du refactoring des modèles, de l'écriture du code et de son refactoring peut facilement aller en parallèle - en une seule itération.

En général, l'approche d'ingénierie n'est plus du tout équivalente au modèle en cascade, ce sont deux choses indépendantes.

L'approche d'ingénierie est facilement combinée avec toute méthodologie d'organisation de développement.

Le blog de Hillel Wayne montre à quel point il est facile de travailler avec des spécifications et des modèles formels. Il a un excellent exemple de la façon de spécifier formellement la logique de l'interface utilisateur d'un programme en 10 minutes et de vérifier certaines de ses propriétés.

Je ne vais pas entrer dans les détails et traduire l'intégralité de l'article, je vais juste montrer la spécification elle-même en alliage :

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
   .