SPARK (linguagem de programação) - SPARK (programming language)

Este artigo é sobre a linguagem de programação . Para a estrutura de computação em cluster que pode ser executada em Scala , Java e Python , consulte Apache Spark .
FAGULHA
Sparkada.jpg
Paradigma Multiparadigma
Desenvolvedor Altran e AdaCore
Versão estável
Comunidade 2021 / 1º de junho de 2021 ; há 4 meses (2021-06-01)
Disciplina de digitação estático , forte , seguro , nominativo
SO Plataforma cruzada : Linux , Microsoft Windows , Mac OS X
Licença GPLv3
Local na rede Internet Sobre SPARK
Implementações principais
SPARK Pro, SPARK GPL Edition, Comunidade SPARK
Influenciado por
Ada , Eiffel

SPARK é uma linguagem de programação de computador formalmente definida baseada na linguagem de programação Ada , destinada ao desenvolvimento de software de alta integridade usado em sistemas onde uma operação previsível e altamente confiável é essencial. Ele facilita o desenvolvimento de aplicativos que exigem proteção, segurança ou integridade nos negócios.

Originalmente, havia três versões da linguagem SPARK (SPARK83, SPARK95, SPARK2005) com base em Ada 83, Ada 95 e Ada 2005, respectivamente.

Uma quarta versão da linguagem SPARK, SPARK 2014, baseada em Ada 2012, foi lançada em 30 de abril de 2014. SPARK 2014 é um redesenho completo da linguagem e ferramentas de verificação de suporte .

A linguagem SPARK consiste em um subconjunto bem definido da linguagem Ada que usa contratos para descrever a especificação de componentes em uma forma que seja adequada para verificação estática e dinâmica.

No SPARK83 / 95/2005, os contratos são codificados em comentários Ada e, portanto, são ignorados por qualquer compilador Ada padrão, mas são processados ​​pelo "Examiner" SPARK e suas ferramentas associadas.

O SPARK 2014, em contraste, usa a sintaxe de "aspecto" embutida do Ada 2012 para expressar contratos, trazendo-os para o núcleo da linguagem. A principal ferramenta do SPARK 2014 (GNATprove) é baseada na infraestrutura GNAT / GCC e reutiliza quase todo o front-end GNAT Ada 2012.

Visão geral técnica

O SPARK utiliza os pontos fortes de Ada enquanto tenta eliminar todas as suas ambigüidades e construções inseguras em potencial. Os programas SPARK foram concebidos para não serem ambíguos e seu comportamento não deve ser afetado pela escolha do compilador Ada . Esses objetivos são alcançados em parte pela omissão de alguns dos recursos mais problemáticos de Ada (como tarefas paralelas irrestritas ) e em parte pela introdução de contratos que codificam as intenções e requisitos do designer de aplicativos para certos componentes de um programa.

A combinação dessas abordagens permite que o SPARK atinja seus objetivos de design, que são:

  • solidez lógica
  • definição formal rigorosa
  • semântica simples
  • segurança
  • poder expressivo
  • verificabilidade
  • requisitos de recursos limitados (espaço e tempo).
  • requisitos mínimos do sistema de tempo de execução

Exemplos de contrato

Considere a especificação do subprograma Ada abaixo: 

procedure Increment (X : in out Counter_Type);

Em Ada puro, isso pode incrementar a variável Xem um ou mil; ou pode definir algum contador global para Xe retornar o valor original do contador em X; ou pode não fazer absolutamente nada com ele X.

Com o SPARK 2014, os contratos são adicionados ao código para fornecer informações adicionais sobre o que um subprograma realmente faz. Por exemplo, podemos alterar a especificação acima para dizer: 

procedure Increment (X : in out Counter_Type)
  with Global => null,
       Depends => (X => X);

Isso especifica que o Incrementprocedimento não usa (nem atualiza nem lê) nenhuma variável global e que o único item de dados usado no cálculo do novo valor de Xé Xele mesmo.

Como alternativa, o designer pode especificar: 

procedure Increment (X : in out Counter_Type)
  with Global  => (In_Out => Count),
       Depends => (Count  => (Count, X),
                   X      => null);

Isso especifica que Incrementusará a variável global Countno mesmo pacote que Increment, que o valor exportado de Countdepende dos valores importados de Counte X, e que o valor exportado de Xnão depende de nenhuma variável e será derivado apenas de dados constantes .

Se o GNATprove for executado na especificação e no corpo correspondente de um subprograma, ele analisará o corpo do subprograma para construir um modelo do fluxo de informações. Este modelo é então comparado com o que foi especificado pelas anotações e quaisquer discrepâncias relatadas ao usuário.

Essas especificações podem ser estendidas ainda mais pela afirmação de várias propriedades que precisam ser mantidas quando um subprograma é chamado ( pré-condições ) ou que serão mantidas quando a execução do subprograma for concluída ( pós-condições ). Por exemplo, poderíamos dizer o seguinte: 

procedure Increment (X : in out Counter_Type)
  with Global  => null,
       Depends => (X => X),
       Pre     => X < Counter_Type'Last,
       Post    => X = X'Old + 1;

Isso, agora, especifica não apenas que Xé derivado de si mesmo, mas também que antes de Incrementser chamado Xdeve ser estritamente menor que o último valor possível de seu tipo e que depois Xserá igual ao valor inicial de Xmais um.

Condições de verificação

GNATprove também pode gerar um conjunto de condições de verificação ou VCs. Essas condições são usadas para estabelecer se certas propriedades são válidas para um determinado subprograma. No mínimo, o GNATprove irá gerar VCs para estabelecer que todos os erros de tempo de execução não podem ocorrer dentro de um subprograma, como:

  • índice de array fora do intervalo
  • violação de faixa de tipo
  • divisão por zero
  • estouro numérico.

Se uma pós-condição ou qualquer outra afirmação for adicionada a um subprograma, GNATprove também gerará VCs que exigem que o usuário mostre que essas propriedades são válidas para todos os caminhos possíveis através do subprograma.

Nos bastidores, GNATprove usa a linguagem intermediária Why3 e VC Generator, e os provadores de teoremas CVC4, Z3 e Alt-Ergo para descarregar VCs. O uso de outros provadores (incluindo verificadores de prova interativos) também é possível por meio de outros componentes do conjunto de ferramentas Why3.

História

A primeira versão do SPARK (baseado em Ada 83) foi produzida na Universidade de Southampton (com patrocínio do Ministério da Defesa do Reino Unido ) por Bernard Carré e Trevor Jennings. O nome SPARK foi derivado de SPADE Ada Kernel , em referência ao subconjunto SPADE da linguagem de programação Pascal .

Posteriormente, a linguagem foi progressivamente ampliada e refinada, primeiro pela Program Validation Limited e depois pela Praxis Critical Systems Limited. Em 2004, a Praxis Critical Systems Limited mudou seu nome para Praxis High Integrity Systems Limited. Em janeiro de 2010, a empresa se tornou Altran Praxis .

No início de 2009, a Praxis formou uma parceria com a AdaCore e lançou o "SPARK Pro" sob os termos da GPL. Em junho de 2009, veio o SPARK GPL Edition 2009, voltado para FOSS e comunidades acadêmicas.

Em junho de 2010, a Altran-Praxis anunciou que a linguagem de programação SPARK seria usada no software do projeto lunar dos EUA CubeSat , com conclusão prevista para 2015.

Em janeiro de 2013, Altran-Praxis mudou seu nome para Altran.

O primeiro lançamento Pro do SPARK 2014 foi anunciado em 30 de abril de 2014, e foi rapidamente seguido pela edição SPARK 2014 GPL, voltada para o FLOSS e comunidades acadêmicas.

Aplicações industriais

Sistemas relacionados à segurança

SPARK tem sido usado em vários sistemas críticos de segurança de alto perfil, cobrindo a aviação comercial ( motores a jato da série Rolls-Royce Trent , o sistema ARINC ACAMS, o Lockheed Martin C130J), aviação militar ( EuroFighter Typhoon , Harrier GR9, AerMacchi M346), ar - gerenciamento de tráfego (sistema UK NATS iFACTS), ferroviário (várias aplicações de sinalização), médicas (o dispositivo de assistência ventricular LifeFlow ) e aplicações espaciais (o projeto Vermont Technical College CubeSat ).

Sistemas relacionados à segurança

O SPARK também tem sido usado no desenvolvimento de sistemas seguros. Os usuários incluem Rockwell Collins (soluções de domínio cruzado Turnstile e SecureOne), o desenvolvimento do MULTOS CA original, o NSA Tokeneer demonstrator, a estação de trabalho secunet multinível, o kernel de separação Muen e o criptografador de dispositivo de bloco Genode.

Em agosto de 2010, Rod Chapman, engenheiro principal da Altran Praxis, implementou Skein , um dos candidatos para SHA-3 , em SPARK. Ao comparar o desempenho das implementações SPARK e C e após cuidadosa otimização, ele conseguiu que a versão SPARK rodasse apenas cerca de 5 a 10% mais lenta do que C. Melhoria posterior no middle-end Ada no GCC (implementado por Eric Botcazou da AdaCore ) fechou a lacuna, com o código SPARK correspondendo exatamente ao C no desempenho.

A NVIDIA também adotou o SPARK para a implementação de firmware de segurança crítica.

Em 2020, Rod Chapman reimplementou a biblioteca criptográfica TweetNaCl no SPARK 2014. A versão SPARK da biblioteca tem uma prova completa de segurança de tipo, segurança de memória e algumas propriedades de correção e mantém algoritmos de tempo constante por toda parte. O código SPARK também é significativamente mais rápido do que TweetNaCl.

Veja também

Referências

Leitura adicional

links externos