Linux Foundation anuncia o lançamento da TLA+ Foundation
A Linux Foundation, uma organização sem fins lucrativos que gerencia vários projetos de código aberto, anunciou o lançamento da TLA+ Foundation, uma organização dedicada a promover a adoção e o desenvolvimento da linguagem de especificação formal TLA+. A AWS, Oracle e Microsoft estão entre os membros fundadores da TLA+ Foundation.
Desenvolvida pela cientista da computação e matemática Leslie Lamport, a TLA+ é uma linguagem única que permite especificar um sistema, em vez de implementar software. Baseada em conceitos matemáticos, principalmente teoria dos conjuntos e lógica temporal, a TLA+ permite a expressão das propriedades de correção desejadas de um sistema de maneira formal e rigorosa.
A TLA+ inclui um verificador de modelo e um provador de teorema para verificar se a especificação de um sistema satisfaz suas propriedades desejadas. Isso ajuda os desenvolvedores a raciocinar sobre sistemas acima do nível do código, descobrindo e prevenindo falhas de projeto antes que evoluam para bugs durante os estágios posteriores da engenharia de software.
A TLA+ Foundation fornecerá recursos de educação e treinamento em torno do TLA+, financiará pesquisas e desenvolverá ferramentas para a linguagem. A Fundação também tomará decisões sobre aprimoramentos de linguagem, abordará o feedback do usuário e orientará a evolução da linguagem. Além disso, a fundação facilitará uma maior colaboração entre a indústria e a academia, avançando o estado da arte em métodos formais e pesquisa de sistemas simultâneos e distribuídos.
A missão da TLA+ Foundation é defender projetos de código aberto, garantindo que a TLA+ continue a evoluir e permaneça acessível à comunidade tecnológica mais ampla. Isso também promoverá sua adoção mais ampla na indústria de tecnologia. A TLA+ já foi usada com sucesso por grandes empresas de tecnologia como Amazon, Oracle e Microsoft para verificar e projetar sistemas em escala planetária.
Certamente, aqui está um exemplo simples de especificação de um sistema usando a linguagem TLA+:
Suponha que queremos especificar um sistema que permite que vários usuários possam compartilhar uma única impressora. Podemos descrever esse sistema em TLA+ usando as seguintes variáveis e ações:
------------------------------ MODULE Printer ------------------------------
EXTENDS Naturals, TLC
VARIABLES queue, printer_busy
Init == queue = <<>> /\ printer_busy = FALSE
Print(user) == queue' = Append(queue, user)
JobDone == printer_busy' = FALSE /\
IF queue = <<>> THEN queue' = <<>> ELSE printer_busy' = TRUE /\ queue' = Tail(queue)
Next == JobDone \/ Print(1)
Spec == Init /\ [][Next]_<<queue, printer_busy>>
=============================================================================
Nesta especificação, temos duas variáveis: queue (fila de usuários) e printer_busy (indicador de impressora ocupada). A ação Init define o estado inicial do sistema, onde a fila está vazia e a impressora não está ocupada. A ação Print(user) adiciona um usuário à fila de impressão. A ação JobDone indica que a impressora terminou de imprimir um trabalho e está pronta para imprimir outro. A ação Next define a próxima ação possível do sistema, que pode ser ou JobDone ou Print(1).
A especificação completa do sistema é dada pela fórmula Spec, que combina o estado inicial Init com uma sequência de ações Next. A notação [][Next]_<<queue, printer_busy>> é uma fórmula de lógica temporal que significa que a ação Next é sempre possível a partir de qualquer estado, e que as variáveis queue e printer_busy devem ser rastreadas ao longo do tempo.
Essa é apenas uma visão geral muito básica da linguagem TLA+. Para especificações mais complexas, a sintaxe pode se tornar mais complicada, mas a ideia geral é a mesma: descrever o comportamento do sistema em termos de variáveis e ações, e definir uma sequência de ações possíveis a partir de qualquer estado inicial.