Digite segurança

Na ciência da computação , a segurança e a integridade do tipo são a medida em que uma linguagem de programação desencoraja ou evita erros de tipo . A segurança de tipo às vezes é considerada alternativamente uma propriedade dos recursos de uma linguagem de computador; isto é, alguns recursos são seguros para o tipo e seu uso não resultará em erros de tipo, enquanto outros recursos na mesma linguagem podem não ser seguros para o tipo e um programa que os utiliza pode encontrar erros de tipo. Os comportamentos classificados como erros de tipo por uma determinada linguagem de programação são geralmente aqueles que resultam de tentativas de realizar operações sobre valores que não são do tipo de dados apropriado , por exemplo, adicionar uma string a um número inteiro quando não há definição de como lidar com este caso . Esta classificação é parcialmente baseada em opiniões.

A imposição de tipo pode ser estática, capturando erros potenciais em tempo de compilação , ou dinâmica, associando informações de tipo a valores em tempo de execução e consultando-os conforme necessário para detectar erros iminentes, ou uma combinação de ambos. [1] A aplicação do tipo dinâmico geralmente permite a execução de programas que seriam inválidos sob a aplicação estática.

No contexto de sistemas de tipo estático (em tempo de compilação), a segurança de tipo geralmente envolve (entre outras coisas) uma garantia de que o valor eventual de qualquer expressão será um membro legítimo do tipo estático dessa expressão. O requisito preciso é mais sutil do que isso – veja, por exemplo, subtipagem e polimorfismo para complicações.

Definições

Intuitivamente, a solidez do tipo é capturada pela declaração incisiva de Robin Milner de que

Programas bem digitados não podem “dar errado”. [2]

Em outras palavras, se um sistema de tipos for sound , então as expressões aceitas por esse sistema de tipos deverão ser avaliadas como um valor do tipo apropriado (em vez de produzir um valor de algum outro tipo não relacionado ou travar com um erro de tipo). Vijay Saraswat fornece a seguinte definição relacionada:

Uma linguagem é de tipo seguro se as únicas operações que podem ser executadas nos dados da linguagem são aquelas sancionadas pelo tipo de dados. [3]

Porém, o que significa exatamente um programa ser "bem digitado" ou "dar errado" são propriedades de sua semântica estática e dinâmica , que são específicas de cada linguagem de programação. Conseqüentemente, uma definição precisa e formal de solidez de tipo depende do estilo de semântica formal usada para especificar uma linguagem. Em 1994, Andrew Wright e Matthias Felleisen formularam o que se tornou a definição padrão e a técnica de prova para segurança de tipos em linguagens definidas pela semântica operacional , [4] que está mais próxima da noção de segurança de tipos conforme entendida pela maioria dos programadores. Sob esta abordagem, a semântica de uma linguagem deve ter as duas propriedades a seguir para ser considerada tipo-som:

Progresso
Um programa bem digitado nunca fica "travado": cada expressão já é um valor ou pode ser reduzida a um valor de alguma forma bem definida. Em outras palavras, o programa nunca entra em um estado indefinido onde nenhuma transição adicional é possível.
Preservação (ou redução de assunto )
Após cada etapa de avaliação, o tipo de cada expressão permanece o mesmo (ou seja, seu tipo é preservado ).

Vários outros tratamentos formais de solidez de tipo também foram publicados em termos de semântica denotacional e semântica operacional estrutural . [2] [5] [6]

Relação com outras formas de segurança

Isoladamente, a solidez do tipo é uma propriedade relativamente fraca, pois essencialmente apenas afirma que as regras de um sistema de tipos são internamente consistentes e não podem ser subvertidas. No entanto, na prática, as linguagens de programação são projetadas de modo que a boa digitação também implique outras propriedades mais fortes, algumas das quais incluem:

  • Prevenção de operações ilegais. Por exemplo, um sistema de tipos pode rejeitar a expressão 3 / "Hello, World"como inválida, porque o operador de divisão não está definido para uma string divisor .
  • Segurança de memória
    • Os sistemas de tipos podem evitar ponteiros selvagens que poderiam surgir de um ponteiro para um tipo de objeto sendo tratado como um ponteiro para outro tipo.
    • Sistemas de tipos mais sofisticados, como aqueles que suportam tipos dependentes , podem detectar e rejeitar acessos fora do limite, evitando potenciais estouros de buffer . [7]
  • Erros lógicos originados na semântica de diferentes tipos. Por exemplo, polegadas e milímetros podem ser armazenados como números inteiros, mas não devem ser substituídos ou adicionados. Um sistema de tipos pode impor dois tipos diferentes de inteiros para eles.

Linguagens com e sem segurança de tipo

A segurança de tipo é geralmente um requisito para qualquer linguagem de brinquedo (ou seja, linguagem esotérica ) proposta em pesquisas acadêmicas sobre linguagens de programação. Muitas linguagens, por outro lado, são grandes demais para provas de segurança do tipo geradas por humanos, pois muitas vezes exigem a verificação de milhares de casos. No entanto, foi provado que algumas linguagens, como a Standard ML , que tem uma semântica definida rigorosamente, atendem a uma definição de segurança de tipo. [8] Acredita -se que algumas outras linguagens, como Haskell, [ discute ] atendem a alguma definição de segurança de tipo, desde que certos recursos de "escape" não sejam usados ​​(por exemplo, unsafePerformIO de Haskell , usado para "escapar" do ambiente restrito usual no qual eu /O é possível, contorna o sistema de tipos e, portanto, pode ser usado para quebrar a segurança do tipo. [9] ) O trocadilho de tipo é outro exemplo desse recurso de "escape". Independentemente das propriedades da definição da linguagem, certos erros podem ocorrer em tempo de execução devido a bugs na implementação ou em bibliotecas vinculadas escritas em outras linguagens; tais erros podem tornar um determinado tipo de implementação inseguro em determinadas circunstâncias. Uma versão inicial da máquina virtual Java da Sun era vulnerável a esse tipo de problema. [3]

Digitação forte e fraca

As linguagens de programação são frequentemente classificadas coloquialmente como de tipo forte ou de tipo fraco (também de tipo fraco) para se referir a certos aspectos da segurança de tipo. Em 1974, Liskov e Zilles definiram uma linguagem fortemente tipada como aquela em que "sempre que um objeto é passado de uma função chamadora para uma função chamada, seu tipo deve ser compatível com o tipo declarado na função chamada". [10] Em 1977, Jackson escreveu: "Em uma linguagem fortemente tipada, cada área de dados terá um tipo distinto e cada processo indicará seus requisitos de comunicação em termos desses tipos." [11] Em contraste, uma linguagem de tipo fraco pode produzir resultados imprevisíveis ou pode realizar conversão implícita de tipo. [12]

Gerenciamento de memória e segurança de tipo

A segurança de tipo está intimamente ligada à segurança da memória . Por exemplo, em uma implementação de uma linguagem que possui algum tipo que permite alguns padrões de bits, mas não outros, um erro de memória de ponteiro pendente permite escrever um padrão de bits que não representa um membro legítimo em uma variável morta do tipo , causando um tipo erro quando a variável é lida. Por outro lado, se a linguagem for segura para a memória, ela não poderá permitir que um número inteiro arbitrário seja usado como ponteiro ; portanto, deve haver um ponteiro ou tipo de referência separado.

Como condição mínima, uma linguagem de tipo seguro não deve permitir ponteiros pendentes entre alocações de tipos diferentes. Mas a maioria das linguagens impõe o uso adequado de tipos de dados abstratos definidos pelos programadores, mesmo quando isso não é estritamente necessário para a segurança da memória ou para a prevenção de qualquer tipo de falha catastrófica. As alocações recebem um tipo que descreve seu conteúdo, e esse tipo é fixo durante a alocação. Isso permite que a análise de alias baseada em tipo infira que as alocações de diferentes tipos são distintas.

A maioria das linguagens com segurança de tipo usam coleta de lixo . Pierce diz, "é extremamente difícil alcançar segurança de tipo na presença de uma operação de desalocação explícita", devido ao problema do ponteiro pendente. [13] No entanto , Rust é geralmente considerado seguro para tipos e usa um verificador de empréstimo para obter segurança de memória, em vez de coleta de lixo.

Digite segurança em linguagens orientadas a objetos

Em linguagens orientadas a objetos, a segurança de tipos geralmente é intrínseca ao fato de que um sistema de tipos está implementado. Isso é expresso em termos de definições de classe.

Uma classe define essencialmente a estrutura dos objetos derivados dela e uma API como um contrato para lidar com esses objetos. Cada vez que um novo objeto é criado ele cumprirá esse contrato.

Cada função que troca objetos derivados de uma classe específica, ou que implementa uma interface específica , aderirá a esse contrato: portanto, nessa função, as operações permitidas naquele objeto serão apenas aquelas definidas pelos métodos da classe que o objeto implementa. Isto garantirá que a integridade do objeto será preservada. [14]

As exceções são as linguagens orientadas a objetos que permitem a modificação dinâmica da estrutura do objeto ou o uso de reflexão para modificar o conteúdo de um objeto para superar as restrições impostas pelas definições dos métodos de classe.

Digite questões de segurança em idiomas específicos

Ada

Ada foi projetada para ser adequada para sistemas embarcados , drivers de dispositivos e outras formas de programação de sistemas , mas também para encorajar a programação com segurança de tipo. Para resolver esses objetivos conflitantes, Ada limita a insegurança de tipo a um determinado conjunto de construções especiais cujos nomes geralmente começam com a string Unchecked_ . Unchecked_Deallocation pode ser efetivamente banido de uma unidade de texto Ada aplicando pragma Pure a esta unidade. Espera-se que os programadores usem construções Unchecked_ com muito cuidado e somente quando necessário; programas que não os utilizam são seguros para o tipo.

A linguagem de programação SPARK é um subconjunto de Ada que elimina todas as suas potenciais ambigüidades e inseguranças e, ao mesmo tempo, adiciona contratos verificados estaticamente aos recursos de linguagem disponíveis. O SPARK evita problemas com ponteiros pendentes , proibindo totalmente a alocação em tempo de execução.

Ada2012 adiciona contratos verificados estaticamente à própria linguagem (na forma de pré e pós-condições, bem como invariantes de tipo).

C

A linguagem de programação C é segura para tipos em contextos limitados; por exemplo, um erro em tempo de compilação é gerado quando é feita uma tentativa de converter um ponteiro para um tipo de estrutura em um ponteiro para outro tipo de estrutura, a menos que uma conversão explícita seja usada. No entanto, diversas operações muito comuns não são seguras para o tipo; por exemplo, a maneira usual de imprimir um número inteiro é algo como printf("%d", 12), onde %dinforma printfem tempo de execução para esperar um argumento inteiro. (Algo como printf("%s", 12), que diz à função para esperar um ponteiro para uma string de caracteres e ainda fornece um argumento inteiro, pode ser aceito pelos compiladores, mas produzirá resultados indefinidos.) Isso é parcialmente mitigado pela verificação de alguns compiladores (como o gcc). correspondências de tipo entre argumentos printf e strings de formato.

Além disso, C, como Ada, fornece conversões explícitas não especificadas ou indefinidas; e diferentemente de Ada, expressões idiomáticas que usam essas conversões são muito comuns e ajudaram a dar ao C uma reputação de tipo inseguro. Por exemplo, a maneira padrão de alocar memória no heap é invocar uma função de alocação de memória, como malloc, com um argumento indicando quantos bytes são necessários. A função retorna um ponteiro não digitado (type void *), que o código de chamada deve converter explícita ou implicitamente para o tipo de ponteiro apropriado. Implementações pré-padronizadas de C exigiam uma conversão explícita para fazê-lo, portanto o código tornou-se uma prática aceita. [15](struct foo *) malloc(sizeof(struct foo))

C++

Alguns recursos do C++ que promovem código com maior segurança de tipo:

C#

C# é seguro para tipos. Possui suporte para ponteiros não digitados, mas deve ser acessado usando a palavra-chave "inseguro", que pode ser proibida no nível do compilador. Possui suporte inerente para validação de conversão em tempo de execução. As conversões podem ser validadas usando a palavra-chave "as" que retornará uma referência nula se a conversão for inválida, ou usando uma conversão no estilo C que lançará uma exceção se a conversão for inválida. Consulte Operadores de conversão C Sharp .

A confiança indevida no tipo de objeto (do qual todos os outros tipos são derivados) corre o risco de anular o propósito do sistema de tipos C#. Geralmente é uma prática melhor abandonar referências de objetos em favor de genéricos , semelhantes aos modelos em C++ e genéricos em Java .

Java

A linguagem Java foi projetada para reforçar a segurança de tipo. Qualquer coisa em Java acontece dentro de um objeto e cada objeto é uma instância de uma classe .

Para implementar a aplicação de segurança de tipo , cada objeto, antes do uso, precisa ser alocado . Java permite o uso de tipos primitivos , mas apenas dentro de objetos alocados adequadamente.

Às vezes, uma parte do tipo de segurança é implementada indiretamente: por exemplo, a classe BigDecimal representa um número de ponto flutuante de precisão arbitrária, mas trata apenas de números que podem ser expressos com uma representação finita. A operação BigDecimal.divide() calcula um novo objeto como a divisão de dois números expressos como BigDecimal.

Neste caso, se a divisão não tiver representação finita, como quando se calcula, por exemplo, 1/3=0,33333..., o método divide() pode gerar uma exceção se nenhum modo de arredondamento for definido para a operação. Conseqüentemente, a biblioteca, e não a linguagem, garante que o objeto respeite o contrato implícito na definição da classe.

ML padrão

O ML padrão tem semântica definida rigorosamente e é conhecido por ser seguro para tipos. No entanto, algumas implementações, incluindo o Standard ML of New Jersey (SML/NJ), sua variante sintática Mythryl e MLton , fornecem bibliotecas que oferecem operações inseguras. Esses recursos são frequentemente usados ​​em conjunto com as interfaces de funções externas dessas implementações para interagir com códigos não-ML (como bibliotecas C) que podem exigir dados dispostos de maneiras específicas. Outro exemplo é o próprio nível superior interativo SML/NJ , que deve usar operações inseguras para executar o código ML inserido pelo usuário.

Módulo-2

Modula-2 é uma linguagem fortemente tipada com uma filosofia de design que exige que qualquer instalação insegura seja explicitamente marcada como insegura. Isto é conseguido "movendo" tais recursos para uma pseudo-biblioteca integrada chamada SYSTEM, de onde devem ser importados antes de poderem ser usados. A importação torna assim visível quando tais instalações são utilizadas. Infelizmente, isto não foi consequentemente implementado no relatório na língua original e na sua implementação. [16] Ainda restavam recursos inseguros, como a sintaxe de conversão de tipo e registros variantes (herdados de Pascal) que poderiam ser usados ​​sem importação prévia. [17] A dificuldade em mover essas facilidades para o pseudomódulo SYSTEM foi a falta de qualquer identificador para a facilidade que pudesse então ser importado, uma vez que apenas identificadores podem ser importados, mas não sintaxe.

 SISTEMA DE IMPORTAÇÃO ;  (* permite o uso de certas instalações inseguras: *) 
Palavra VAR  : SYSTEM . PALAVRA ; endereço : SISTEMA . ENDEREÇO ​​; endereço := SISTEMA . ADR ( palavra );     
  

(* mas a sintaxe de conversão de tipo pode ser usada sem essa importação *) 
VAR  i  :  INTEGER ;  n  :  CARDEAL ; 
n  :=  CARDEAL ( eu );  (* ou *)  i  :=  INTEGER ( n );

O padrão ISO Modula-2 corrigiu isso para o recurso de conversão de tipo alterando a sintaxe de conversão de tipo para uma função chamada CAST que deve ser importada do pseudomódulo SYSTEM. No entanto, outras instalações inseguras, como registros de variantes, permaneceram disponíveis sem qualquer importação do pseudomódulo SYSTEM. [18]

 SISTEMA DE IMPORTAÇÃO ; 
VARi  : INTEIRO  ; _ n : CARDEAL ; eu := SISTEMA . CAST ( INTEIRO , n ); (*Tipo fundido em ISO Modula-2*)    
    

Uma revisão recente da linguagem aplicou rigorosamente a filosofia de design original. Primeiro, o pseudomódulo SYSTEM foi renomeado para UNSAFE para tornar mais explícita a natureza insegura das instalações importadas de lá. Em seguida, todas as instalações inseguras restantes foram totalmente removidas (por exemplo, registros de variantes) ou movidas para o pseudomódulo INSEGURO. Para instalações onde não há identificador que possa ser importado, foram introduzidos identificadores habilitadores. Para habilitar tal recurso, seu identificador de habilitação correspondente deve ser importado do pseudomódulo UNSAFE. Nenhuma instalação insegura permanece no idioma que não exija importação de UNSAFE. [17]

IMPORTAR  INSEGURO ; 
VARi  : INTEIRO  ; _ n : CARDEAL ; eu : = INSEGURO . CAST ( INTEIRO , n ); (* Tipo lançado em Modula-2 Revisão 2010 *)    
    

DA  IMPORTAÇÃO INSEGURA  FFI ; (* identificador de habilitação para recurso de interface de função externa *) <*FFI="C"*> (* pragma para interface de função externa para C *)  
 

Pascal

Pascal teve vários requisitos de segurança de tipo, alguns dos quais são mantidos em alguns compiladores. Onde um compilador Pascal dita "digitação estrita", duas variáveis ​​não podem ser atribuídas uma à outra, a menos que sejam compatíveis (como a conversão de número inteiro em real) ou atribuídas ao subtipo idêntico. Por exemplo, se você tiver o seguinte fragmento de código:

digite 
TwoTypes = registro I : Inteiro ; P : Verdadeiro ; fim ;    
      
      
  

  DualTypes = registro I : Inteiro ; P : Verdadeiro ; fim ;  
     
     
  

var 
T1 , T2 : DoisTipos ; D1 , D2 : DualTypes ;     
     

Sob digitação estrita, uma variável definida como TwoTypes não é compatível com DualTypes (porque eles não são idênticos, mesmo que os componentes desse tipo definido pelo usuário sejam idênticos) e uma atribuição de é ilegal. Uma atribuição de seria legal porque os subtipos para os quais eles são definidos são idênticos. No entanto, uma atribuição como essa seria legal. T1 := D2;T1 := T2;T1.Q := D1.Q;

Lisp comum

Em geral, Common Lisp é uma linguagem de tipo seguro. Um compilador Common Lisp é responsável por inserir verificações dinâmicas para operações cuja segurança de tipo não pode ser comprovada estaticamente. Entretanto, um programador pode indicar que um programa deve ser compilado com um nível mais baixo de verificação dinâmica de tipo. [19] Um programa compilado nesse modo não pode ser considerado seguro de tipo.

Exemplos de C++

Os exemplos a seguir ilustram como os operadores de conversão C++ podem quebrar a segurança de tipo quando usados ​​incorretamente. O primeiro exemplo mostra como os tipos de dados básicos podem ser convertidos incorretamente:

#include <iostream> usando namespace std ; 
  

int principal () { int ival = 5 ; // valor inteiro float fval = reinterpret_cast < float &> ( ival ); // reinterpreta o padrão de bits cout << fval << endl ; // gera o inteiro como float return 0 ; }   
                                       
        
                                
     

Neste exemplo, reinterpret_castimpede explicitamente que o compilador execute uma conversão segura de valor inteiro em valor de ponto flutuante. [20] Quando o programa é executado, ele produzirá um valor de ponto flutuante lixo. O problema poderia ter sido evitado escrevendofloat fval = ival;

O próximo exemplo mostra como as referências de objetos podem ser downcast incorretamente:

#include <iostream> usando namespace std ; 
  

class Parent { public : virtual ~ Parent () {} // destruidor virtual para RTTI };  

       


classe Filho1 : público Pai { público : int a ; };     

     


classe Filho2 : público Pai { público : float b ; };     

     


int principal () { Filho1 c1 ; c1 . uma = 5 ; Pai & p = c1 ; // upcast sempre seguro Child2 & c2 = static_cast < Child2 &> ( p ); // downcast cout inválido << c2 . b << fim ; // produzirá dados inúteis return 0 ; }   
     
      
                             
         
                  
     

As duas classes filhas possuem membros de tipos diferentes. Ao fazer downcast de um ponteiro de classe pai para um ponteiro de classe filho, o ponteiro resultante pode não apontar para um objeto válido do tipo correto. No exemplo, isso faz com que o valor lixo seja impresso. O problema poderia ter sido evitado substituindo-o static_castpor dynamic_castuma exceção em conversões inválidas. [21]

Veja também

Notas

  1. ^ "O que saber antes de debater sistemas de tipos | Ovid [blogs.perl.org]" . blogs.perl.org . Recuperado em 27/06/2023 .
  2. ^ ab Milner, Robin (1978), "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences , 17 (3): 348–375, doi : 10.1016/0022-0000(78)90014-4 , hdl : 20.500.11820/d16745d7-f113-44f0-a7a3-687c2b709f66
  3. ^ ab Saraswat, Vijay (15/08/1997). "Java não é seguro para tipos" . Recuperado em 08/10/2008 .
  4. ^ Wright, AK; Felleisen, M. (15 de novembro de 1994). "Uma abordagem sintática para digitar solidez". Informação e Computação . 115 (1): 38–94. doi : 10.1006/inco.1994.1093 . ISSN0890-5401  .
  5. ^ Damas, Luís; Milner, Robin (25 de janeiro de 1982). "Principais esquemas de tipos para programas funcionais". Anais do 9º simpósio ACM SIGPLAN-SIGACT sobre Princípios de linguagens de programação - POPL '82 . Associação de Máquinas de Computação. pp. 207–212. doi :10.1145/582153.582176. ISBN 0897910656. S2CID11319320  .
  6. ^ Tofte, Mads (1988). Semântica Operacional e Inferência de Tipos Polimórficos (Tese).
  7. ^ Henriksen, Troels; Elsman, Martin (17 de junho de 2021). "Rumo a tipos dependentes de tamanho para programação de array". Anais do 7º Workshop Internacional ACM SIGPLAN sobre Bibliotecas, Linguagens e Compiladores para Programação de Array . Associação de Máquinas de Computação. páginas 1–14. doi :10.1145/3460944.3464310. ISBN 9781450384667. S2CID235474098  .
  8. ^ ML padrão. Smlnj.org. Obtido em 02/11/2013.
  9. ^ "System.IO.Inseguro" . Manual de bibliotecas GHC: base-3.0.1.0 . Arquivado do original em 05/07/2008 . Recuperado em 17/07/2008 .
  10. ^ Liskov, B; Zilles, S (1974). “Programação com tipos de dados abstratos”. Avisos da ACM SIGPLAN . 9 (4): 50–59. CiteSeerX 10.1.1.136.3043 . doi :10.1145/942572.807045. 
  11. ^ Jackson, K. (1977). “Processamento paralelo e construção modular de software”. Projeto e Implementação de Linguagens de Programação . Notas de aula em Ciência da Computação. Vol. 54. pp. doi :10.1007/BFb0021435. ISBN 3-540-08360-X.
  12. ^ "CS1130. Transição para programação OO. - Primavera de 2012 - versão individualizada" . Universidade Cornell, Departamento de Ciência da Computação. 2005 . Recuperado em 15/09/2023 .
  13. ^ Pierce, Benjamin C. (2002). Tipos e linguagens de programação . Cambridge, Massachusetts: MIT Press. pág. 158. ISBN 0-262-16209-1.
  14. ^ A segurança de tipo é, portanto, também uma questão de boa definição de classe: métodos públicos que modificam o estado interno de um objeto devem preservar a integridade do objeto
  15. ^ Kernighan ; Dennis M. Ritchie (março de 1988). A linguagem de programação C (2ª ed.). Englewood Cliffs, NJ : Prentice Hall . pág. 116. ISBN 978-0-13-110362-7. Em C, o método apropriado é declarar que malloc retorna um ponteiro para void e, em seguida, coagir explicitamente o ponteiro para o tipo desejado com uma conversão.
  16. ^ Niklaus Wirth (1985). Programação em Modula-2 . Springer Verlag.
  17. ^ ab "A Separação entre Instalações Seguras e Inseguras" . Recuperado em 24 de março de 2015 .
  18. ^ "Referência da linguagem ISO Modula-2" . Recuperado em 24 de março de 2015 .
  19. ^ "HiperSpec Lisp comum" . Recuperado em 26 de maio de 2013 .
  20. ^ "conversão reinterpret_cast - cppreference.com" . En.cppreference.com . Recuperado em 21/09/2022 .
  21. ^ "conversão dinâmica_cast - cppreference.com" . En.cppreference.com . Recuperado em 21/09/2022 .

Referências

  • Pierce, Benjamin C. (2002). Tipos e linguagens de programação. Imprensa do MIT. ISBN 978-0-262-16209-8.
  • "Digite Seguro". Wiki do repositório de padrões de Portland .
  • Wright, Andrew K.; Matthias Felleisen (1994). "Uma abordagem sintática para digitar solidez". Informação e Computação . 115 (1): 38–94. doi : 10.1006/inco.1994.1093 .
  • Macrakis, Stavros (abril de 1982). “Segurança e potência”. Notas de engenharia de software ACM SIGSOFT . 7 (2): 25–26. doi :10.1145/1005937.1005941. S2CID10426644  .
Obtido em "https://en.wikipedia.org/w/index.php?title=Type_safety&oldid=1193889154"