↙️ 🛩️ 😇 Enfoque de ingeniería para el desarrollo de software 🧒🏿 🏩 🕢

¿Cómo probar ideas, arquitectura y algoritmos sin escribir código? ¿Cómo formular y verificar sus propiedades? ¿Qué son los verificadores de modelos y los buscadores de modelos? Requisitos y especificaciones: ¿una reliquia del pasado?

Hola Mi nombre es Vasil Dyadov, ahora trabajo como programador en Yandex, antes de eso trabajé en Intel, solía desarrollar código RTL (nivel de transferencia de registro) en Verilog / VHDL para ASIC / FPGA. Hace tiempo que me gusta el tema de la confiabilidad del software y el hardware, las matemáticas, las herramientas y los métodos utilizados para desarrollar software y lógica con propiedades garantizadas y predefinidas.

Este es mi primer artículo de una serie diseñada para llamar la atención de los desarrolladores y gerentes sobre el enfoque de ingeniería para el desarrollo de software. Recientemente, ha sido ignorado inmerecidamente, a pesar de los cambios revolucionarios en su enfoque y herramientas de apoyo.

No voy a disimular: la tarea principal del artículo es despertar interés. Por lo tanto, habrá un mínimo de razonamiento extenso y un máximo de especificidad.

El artículo tiene dos partes. En el primero describiré lo que quiero decir con el enfoque de ingeniería, en el segundo mostraré un ejemplo del uso del enfoque en el marco de una tarea simple (cerca del campo de la arquitectura de microservicios).

Siempre estoy abierto a discutir temas relacionados con el desarrollo de software, y estaré encantado de conversar con los lectores (las coordenadas para la comunicación están en mi perfil).

Parte 1. Enfoque de ingeniería para el desarrollo

Que es esto Te mostraré el ejemplo de construir un puente:

La etapa 1 es la recopilación de requisitos para el puente: el tipo de puente, la capacidad de carga, etc.
Etapa 2: especificación de requisitos y cálculo de estructuras (especificación).
Etapa 3: la construcción en sí misma basada en cálculos de ingeniería (especificaciones).

Por supuesto, esta es una analogía simplificada. Nadie hace puentes prototipo para aclarar requisitos y especificaciones. La parametrización no se puede agregar al puente para que se arquee o suspenda. Pero en general, creo que la analogía es clara.

En el desarrollo de software, los pasos 1 y 2 a menudo están ausentes o muy poco expresados. Si los requisitos son fijos, entonces es vago, incompleto e informal. Solo unos pocos requisitos detallados y desarrollar especificaciones claras.

Mucha gente piensa que esto es una pérdida de tiempo, una reliquia del pasado, especialmente si se elige el enfoque ágil para el desarrollo (especialmente con iteraciones cortas). Y este es un gran error.

Por qué

Para comenzar, entenderemos cuáles son tales requisitos y especificaciones y cuál es su diferencia significativa, lo que no siempre es obvio para muchos profesionales.

Cuales son los requisitos?

En resumen, los requisitos son la formulación de las propiedades del producto en términos del área temática. Por ejemplo, así: "Todas las instancias del programa deben procesar igualmente las solicitudes de entrada".

Los requisitos no utilizan los términos del alcance de la implementación. Tan pronto como los términos "sincronización de estado", Raft, Paxos, "complejidad logarítmica en el tiempo" se filtren en los requisitos, entonces los requisitos y la especificación comienzan a mezclarse.

Es importante comprender esto y separar claramente uno del otro.

Por qué

Los requisitos deben ser claros para los consumidores de software, por lo tanto, deben ser del área temática para la que se está desarrollando el software (a menudo, los expertos que están lejos del desarrollo deben participar en la formulación de requisitos y establecer una tarea para el desarrollo de software).
Las propiedades de software que ve un consumidor se evalúan mediante métricas de área temática. Es necesario separar los requisitos y especificaciones para poder 1) identificar las principales métricas del producto mediante las cuales el consumidor evaluará nuestro software, y 2) comprender claramente qué propiedades del producto son importantes para el usuario y cuáles no.

De lo contrario, puede resultar así: los desarrolladores, que no cumplan con la fecha límite, sacrificarán propiedades importantes y dedicarán mucho tiempo y atención a las que no son importantes. Además, lo que parece importante desde el punto de vista del desarrollo de software puede no ser importante desde el punto de vista del usuario.

Un ejemplo clásico de tal discrepancia se da en una variedad de literatura sobre desarrollo de interfaz de usuario y en artículos (por ejemplo: Tiempo de respuesta del sistema y satisfacción del usuario: un estudio experimental de aplicaciones basadas en navegador , latencia de computadora: 1977–2017 ). Los desarrolladores generalmente intentan optimizar el tiempo de ejecución de una operación, por ejemplo, buscando información en una base de datos, y el tiempo de respuesta del usuario es importante. Y si la búsqueda es lenta, pero el usuario comienza a ver los resultados devueltos lo más rápido posible, entonces le parece que dicho software funciona mejor que el que busca rápidamente, pero primero acumula los resultados y finalmente los muestra a todos.

Es por eso que los planificadores de recursos del sistema operativo difieren para los modos operativos de servidor y escritorio. Para el modo de servidor, el rendimiento máximo del sistema es importante, es decir, la optimización del tiempo y la memoria para utilizar el servidor de manera eficiente. Y para el usuario, la demora en la respuesta del sistema es importante. Cuanto más rápido responde el sistema a las acciones, más rápido parece, incluso si funciona más lento.

Y finalmente, la razón más importante:

Si los requisitos y las especificaciones son mixtos, significa que no entendemos completamente las tareas para las que estamos desarrollando software. Comenzamos a formular y resolver problemas del área temática en el campo del desarrollo de software. Por lo tanto, la lógica de dominio se filtra y confunde la lógica del código. El resultado es un código estrechamente acoplado que es difícil de mantener.

Esto fue bien escrito por Michael Jackson en el libro Marcos de problemas: análisis y estructuración de problemas de desarrollo de software . En mi opinión, este es uno de los libros más útiles para desarrolladores de software. En primer lugar, enseña a analizar los problemas de los usuarios, que un buen software debería resolver. Un programa súper rápido que consume pocos recursos del sistema pero no resuelve las tareas del usuario es un mal programa. Genial pero malo.

¿Cuál es la especificación?

Una especificación es una formulación de propiedades de software en términos de un campo de desarrollo de software. Aquí es donde los conceptos de complejidad, sincronización, etc.

Las especificaciones se pueden organizar jerárquicamente: de abstracto a específico, en el que puede escribir código. Este enfoque es a menudo el más efectivo. Las especificaciones abstractas reflejan fácilmente la arquitectura: puede ver las propiedades básicas, encontrar errores arquitectónicos, etc. Por lo tanto, podemos encontrar problemas en las primeras etapas del ciclo de vida del software y reducir significativamente el costo de corregir errores.

Cabe destacar especialmente el beneficio y la importancia de las especificaciones para protocolos e interfaces entre los componentes del sistema, lo que ayudará a evitar estas situaciones:

¿Cuál es la diferencia con el enfoque de desarrollo habitual?

En el enfoque de ingeniería, diseñamos el software con las características requeridas de acuerdo con las especificaciones. Verificamos las especificaciones de las propiedades necesarias que provienen de los requisitos.

Hice una comparación en forma de tableta (muy subjetiva):

Propiedad	Enfoque de ingeniería	Enfoque artesanal
Declaración de requisitos	Formato ReqIF detallado y de uso frecuente y herramientas relacionadas (Eclipse RMF, por ejemplo)	Los detalles son generalmente pequeños, la redacción es inexacta, informal
Especificaciones	A menudo se utilizan métodos formales, B, Z, VDM, TLA +, Aleación, etc.	Que eres ¿Qué especificaciones? Escribimos en el archivo lo que debemos hacer y cómo debería funcionar, y eso es suficiente
Especificaciones de depuración y modelado	Pro-B, Atelier B, TLA + / TLC, Alloy, PRISM, VECS, etc.	Oh, ¿cómo podría ser así?
Métricas destacadas	Detallado, basado en especificaciones y modelos.	Bueno, presentaremos algunas métricas, escriba en la página wiki
Desarrollo de código	Basado en especificaciones y modelos	Bueno, aquí como siempre: clap-clap - y en producción
Prueba	Pruebas específicas basadas en modelos para casos límite identificados en modelos; direccional aleatorizado generado por modelo. Integración para casos extremos de acuerdo con las especificaciones de interfaces y protocolos de interacción. Máquinas de supervisión basadas en propiedades LTL de modelos; fuzzing direccional; Verificación del modelo acotado (Divino, por ejemplo)	Bueno, como siempre: un poco de pruebas unitarias, luego pensaremos en casos típicos y agregaremos integración y sistemas; fuzzing para algunas funciones críticas (¿fuzzly débil para encontrar un error de sincronización en software multiproceso?); conducimos pruebas bajo desinfectantes un poco
Verificación	Por ejemplo, tome GNATprove o Frama-C, tome propiedades de las especificaciones, anote el código y pruebe formalmente que el código cumple con las especificaciones formales; o usaremos Atelier B para pasar iterativamente de la especificación a la implementación a través de la generación de código en la etapa final; o elige otro método	No, es aterrador, largo y costoso, y no formulamos las propiedades para la verificación formal: ¿para qué cumplimiento verificar?

¿Y no es el modelo de agitación para un modelo de desarrollo en cascada aquí?

La ingeniería de software, que incluye incluso especificaciones formales y simulaciones, va bien con el enfoque ágil.

Se cree que el enfoque de ingeniería para el desarrollo es incompatible con el desarrollo de software iterativo rápido (como se indica en muchos artículos, aquí hay un ejemplo ).

Pero esto no es así. El enfoque de ingeniería se ha aplicado con éxito en muchos proyectos, incluidos los proyectos con iteraciones cortas.

Anteriormente, debido a medios poco desarrollados y herramientas de soporte, el enfoque de ingeniería estaba estrechamente relacionado con el modelo de cascada.

Pero ahora todo ha cambiado dramáticamente.

Gracias a los éxitos revolucionarios en el campo del modelado, los solucionadores SAT / SMT, etc., ahora es posible verificar rápidamente grandes espacios de estados del sistema para detectar la presencia de las propiedades que necesitamos y la ausencia de propiedades innecesarias, verificar los volúmenes industriales del código, etc.

Aparecieron herramientas industriales de primera clase como Alloy, TLA + / TLC, Atelier B, PRISM, que transfirieron la tarea de formalizar y verificar las especificaciones académicas / matemáticas, que requieren altas calificaciones y grandes esfuerzos, a la tarea de botón, accesible para la mayoría de los programadores.

Las especificaciones ahora se pueden desarrollar de forma iterativa e incremental. Los modelos están bien diseñados de forma iterativa, desde lo abstracto hasta lo concreto. El tiempo de simulación de sistemas incluso grandes se calcula en minutos y horas.

Los requisitos son fáciles de especificar de forma iterativa, especialmente con enfoques y herramientas modernos.
Y el refinamiento de los requisitos, especificaciones, refactorización de modelos, escritura de código y su refactorización pueden ir fácilmente en paralelo, dentro de una iteración.

En general, el enfoque de ingeniería ahora no es en absoluto igual al modelo en cascada, estas son dos cosas independientes.

El enfoque de ingeniería se combina fácilmente con cualquier metodología de organización de desarrollo.

El blog de Hillel Wayne muestra lo fácil que es trabajar con especificaciones y modelos formales. Tiene un gran ejemplo de cómo especificar formalmente la lógica de la interfaz de usuario de un programa en 10 minutos y verificar algunas de sus propiedades.

No entraré en detalles y traduciré el artículo completo, solo mostraré las especificaciones en Alloy :

Especificación de la interfaz de usuario

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, : , , .

, — , , - .

, , .

$\big\{x,y\big\}$ , $x \in X$ $y \in Y$ .

Alloy : X->Y.

( util/relation):

relation.als

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, , , :

graph.als

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:

compgraph.als

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) .

compgraph.als

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]
}

, .

;
;
;
;
;
.

. . : .

, ? ?

, , .

, .

, :

( , );
;
;
.

, .

-> ;
-> ;
-> ;
-> .

, .

, : , . - , — , / .

, : -> .

, :

;
.

, .

, 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" , $2^{168}$ . 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

, r1, — disconnect, r2 — . , r1, r2, r2 .

, — from->to, source ( from) .

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

, :

connect

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.

— , — . from->to.

, connect (, , ).

connect:

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. , :

diconnect

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). .

, , , . .

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

Alloy

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

Hillel Wayne
. , . , .

. . , . . , . . .
, , .

Alloy

Alloy Analyzer + Higher-Order Alloy
Alloy.
Online Tutorial
, .
Tutorial Materials
.

Enfoque de ingeniería para el desarrollo de software

Parte 1. Enfoque de ingeniería para el desarrollo

Cuales son los requisitos?

¿Cuál es la especificación?

¿Cuál es la diferencia con el enfoque de desarrollo habitual?

¿Y no es el modelo de agitación para un modelo de desarrollo en cascada aquí?

2. Alloy

?

?

?

Alloy?

Alloy

Alloy

More articles: