Este artigo é uma tradução . Mas antes dela uma pequena introdução. Como os zumbis são formados? Todos se depararam com uma situação em que querem elevar um amigo ou colega ao seu nível, mas não dá certo. E não é tanto com você, mas com ele que “não dá certo”: de um lado da balança está o salário normal, as tarefas e assim por diante, e do outro, a necessidade de pensar. Pensar é desagradável e doloroso. Ele desiste rapidamente e continua a escrever código sem ligar o cérebro. Você imagina quanto esforço é necessário para superar a barreira do desamparo aprendido e simplesmente não o faz. É assim que se formam os zumbis, que, ao que parece, podem ser curados, mas parece que ninguém vai fazer isso.
Quando eu vi isso (sim, o mesmo camarada dos livros didáticos) e não faz um relatório, mas uma sessão de perguntas e respostas, fiquei um pouco cauteloso. Por precaução, Leslie é um cientista mundialmente famoso, autor de obras fundamentais em computação distribuída, e você também pode conhecê-lo pelas letras La na palavra LaTeX - “Lamport TeX”. O segundo fator alarmante é sua exigência: todos que vierem devem (totalmente de graça) ouvir alguns de seus relatórios com antecedência, fazer pelo menos uma pergunta sobre eles e só então vir. Decidi ver o que Lamport estava transmitindo lá - e é ótimo! É exatamente isso, a pílula mágica para curar zumbis. Já aviso: pelo texto, os amantes de metodologias superflexíveis e os que não gostam de testar o que está escrito podem se esgotar notavelmente.
Depois do habrokat, de fato, começa a tradução do seminário. Gostar de ler!
Qualquer que seja a tarefa que você assuma, você sempre precisa passar por três etapas:
- decida qual objetivo você deseja alcançar;
- decida como você alcançará seu objetivo;
- venha ao seu objetivo.
Isso também se aplica à programação. Quando escrevemos código, precisamos:
- decidir o que o programa deve fazer;
- determinar como deve executar sua tarefa;
- escreva o código correspondente.
A última etapa, claro, é muito importante, mas não vou falar dela hoje. Em vez disso, discutiremos os dois primeiros. Todo programador os executa antes de começar a trabalhar. Você não se senta para escrever a menos que tenha decidido se está escrevendo um navegador ou um banco de dados. Uma certa ideia do objetivo deve estar presente. E você definitivamente pensa sobre o que exatamente o programa fará e não escreve de alguma forma na esperança de que o código de alguma forma se transforme em um navegador.
Como exatamente esse pensamento prévio do código acontece? Quanto esforço devemos colocar nisso? Tudo depende de quão complexo é o problema que estamos resolvendo. Suponha que queremos escrever um sistema distribuído tolerante a falhas. Nesse caso, devemos pensar cuidadosamente antes de nos sentarmos para codificar. E se precisarmos apenas incrementar uma variável inteira em 1? À primeira vista, tudo é trivial aqui, e nenhum pensamento é necessário, mas então lembramos que pode ocorrer um estouro. Portanto, mesmo para entender se um problema é simples ou complexo, primeiro você precisa pensar.
Se você pensar em possíveis soluções para o problema com antecedência, poderá evitar erros. Mas isso requer que seu pensamento seja claro. Para conseguir isso, você precisa anotar seus pensamentos. Gosto muito da citação de Dick Guindon: “Quando você escreve, a natureza mostra como seu pensamento é desleixado”. Se você não escreve, você só pensa que está pensando. E você precisa anotar seus pensamentos na forma de especificações.
As especificações desempenham muitas funções, especialmente em grandes projetos. Mas vou falar apenas de um deles: eles nos ajudam a pensar com clareza. Pensar com clareza é muito importante e bastante difícil, então aqui precisamos de ajuda. Em que idioma devemos escrever as especificações? Em geral, essa é sempre a primeira pergunta dos programadores: em que linguagem vamos escrever. Não há uma resposta correta para isso: os problemas que estamos resolvendo são muito diversos. Para alguns, TLA+ é uma linguagem de especificação que desenvolvi. Para outros, é mais conveniente usar o chinês. Tudo depende da situação.
Mais importante é outra questão: como conseguir um pensamento mais claro? Resposta: Devemos pensar como cientistas. Esta é uma maneira de pensar que se provou ao longo dos últimos 500 anos. Na ciência, construímos modelos matemáticos da realidade. A astronomia foi talvez a primeira ciência no sentido estrito da palavra. No modelo matemático usado na astronomia, os corpos celestes aparecem como pontos com massa, posição e momento, embora na realidade sejam objetos extremamente complexos com montanhas e oceanos, marés e marés. Este modelo, como qualquer outro, foi criado para resolver alguns problemas. É ótimo para determinar para onde apontar o telescópio se precisar encontrar um planeta. Mas se você quiser prever o clima neste planeta, esse modelo não funcionará.
A matemática nos permite determinar as propriedades de um modelo. E a ciência mostra como essas propriedades se relacionam com a realidade. Vamos falar sobre nossa ciência, a ciência da computação. A realidade com a qual trabalhamos são sistemas computacionais de vários tipos: processadores, consoles de jogos, computadores, programas executores e assim por diante. Falarei sobre a execução de um programa em um computador, mas, em geral, todas essas conclusões se aplicam a qualquer sistema de computação. Em nossa ciência, usamos muitos modelos diferentes: a máquina de Turing, conjuntos de eventos parcialmente ordenados e muitos outros.
O que é um programa? Este é qualquer código que pode ser considerado independentemente. Suponha que precisamos escrever um navegador. Realizamos três tarefas: projetamos a visão do programa para o usuário, depois escrevemos o diagrama de alto nível do programa e, finalmente, escrevemos o código. À medida que escrevemos o código, percebemos que precisamos escrever um formatador de texto. Aqui, novamente, precisamos resolver três problemas: determinar qual texto essa ferramenta retornará; selecione um algoritmo para formatação; escrever código. Esta tarefa tem sua própria subtarefa: inserir corretamente um hífen nas palavras. Também resolvemos essa subtarefa em três etapas - como você pode ver, elas são repetidas em vários níveis.
Vamos considerar com mais detalhes o primeiro passo: qual problema o programa resolve. Aqui, na maioria das vezes, modelamos um programa como uma função que recebe alguma entrada e produz alguma saída. Em matemática, uma função é geralmente descrita como um conjunto ordenado de pares. Por exemplo, a função de quadratura para números naturais é descrita como o conjunto {<0,0>, <1,1>, <2,4>, <3,9>, …}. O domínio de tal função é o conjunto dos primeiros elementos de cada par, ou seja, os números naturais. Para definir uma função, precisamos especificar seu escopo e fórmula.
Mas funções em matemática não são iguais a funções em linguagens de programação. A matemática é muito mais fácil. Como não tenho tempo para exemplos complexos, vamos considerar um simples: uma função em C ou um método estático em Java que retorna o máximo divisor comum de dois inteiros. Na especificação deste método, escreveremos: calcula GCD(M,N) para argumentos M и NOnde GCD(M,N) - uma função cujo domínio é o conjunto de pares de inteiros, e o valor de retorno é o maior inteiro divisível por M и N. Como esse modelo se relaciona com a realidade? O modelo opera em números inteiros, enquanto em C ou Java temos um de 32 bits int. Este modelo nos permite decidir se o algoritmo está correto GCD, mas não evitará erros de estouro. Isso exigiria um modelo mais complexo, para o qual não há tempo.
Vamos falar sobre as limitações de uma função como modelo. Alguns programas (como sistemas operacionais) não retornam apenas um determinado valor para determinados argumentos, eles podem ser executados continuamente. Além disso, a função como modelo não é adequada para a segunda etapa: planejar como resolver o problema. A classificação rápida e a classificação por bolha calculam a mesma função, mas são algoritmos completamente diferentes. Portanto, para descrever como o objetivo do programa é alcançado, utilizo um modelo diferente, vamos chamá-lo de modelo comportamental padrão. O programa nele é representado como um conjunto de todos os comportamentos permitidos, cada um dos quais, por sua vez, é uma sequência de estados, e o estado é a atribuição de valores às variáveis.
Vamos ver como seria a segunda etapa do algoritmo de Euclides. precisamos calcular GCD(M, N). nós inicializamos M como xE N como y, então subtraia repetidamente a menor dessas variáveis da maior até que sejam iguais. Por exemplo, se M = 12E N = 18, podemos descrever o seguinte comportamento:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
E se M = 0 и N = 0? Zero é divisível por todos os números, então não há maior divisor neste caso. Nessa situação, precisamos voltar ao primeiro passo e perguntar: precisamos mesmo calcular o GCD para números não positivos? Se isso não for necessário, basta alterar a especificação.
Aqui devemos fazer uma pequena digressão sobre produtividade. Geralmente é medido pelo número de linhas de código escritas por dia. Mas seu trabalho é muito mais útil se você se livrar de um certo número de linhas, porque você tem menos espaço para bugs. E a maneira mais fácil de se livrar do código é na primeira etapa. É perfeitamente possível que você simplesmente não precise de todos os sinos e assobios que está tentando implementar. A maneira mais rápida de simplificar um programa e economizar tempo é não fazer coisas que não deveriam ser feitas. A segunda etapa é o segundo maior potencial de economia de tempo. Se você medir a produtividade em termos de linhas escritas, pensar em como realizar uma tarefa fará com que você menos produtivo, porque você pode resolver o mesmo problema com menos código. Não posso dar estatísticas exatas aqui, pois não tenho como contar o número de linhas que não escrevi devido ao fato de ter gasto tempo na especificação, ou seja, no primeiro e segundo passos. E o experimento também não pode ser montado aqui, porque no experimento não temos o direito de completar a primeira etapa, a tarefa é predeterminada.
É fácil ignorar muitas dificuldades em especificações informais. Não há nada difícil em escrever especificações estritas para funções, não vou discutir isso. Em vez disso, falaremos sobre como escrever especificações fortes para comportamentos padrão. Existe um teorema que diz que qualquer conjunto de comportamentos pode ser descrito usando a propriedade de segurança (segurança) e propriedades de sobrevivência (vivacidade). Segurança significa que nada de ruim acontecerá, o programa não dará uma resposta incorreta. Sobrevivência significa que, mais cedo ou mais tarde, algo bom acontecerá, ou seja, o programa dará a resposta correta mais cedo ou mais tarde. Como regra, a segurança é um indicador mais importante, os erros ocorrem com mais frequência aqui. Portanto, para economizar tempo, não falarei sobre capacidade de sobrevivência, embora, claro, também seja importante.
Alcançamos a segurança prescrevendo, primeiro, o conjunto de possíveis estados iniciais. E segundo, relacionamentos com todos os próximos estados possíveis para cada estado. Vamos agir como cientistas e definir estados matematicamente. O conjunto de estados iniciais é descrito por uma fórmula, por exemplo, no caso do algoritmo de Euclides: (x = M) ∧ (y = N). Para determinados valores M и N existe apenas um estado inicial. A relação com o próximo estado é descrita por uma fórmula na qual as variáveis do próximo estado são escritas com aspas e as variáveis do estado atual são escritas sem aspas. No caso do algoritmo de Euclides, trataremos da disjunção de duas fórmulas, em uma das quais x é o maior valor, e no segundo - y:
No primeiro caso, o novo valor de y é igual ao valor anterior de y, e obtemos o novo valor de x subtraindo a variável menor da variável maior. No segundo caso, fazemos o contrário.
Vamos voltar ao algoritmo de Euclides. Vamos supor novamente que M = 12, N = 18. Isso define um único estado inicial, (x = 12) ∧ (y = 18). Em seguida, inserimos esses valores na fórmula acima e obtemos:
Aqui está a única solução possível: x' = 18 - 12 ∧ y' = 12e obtemos o comportamento: [x = 12, y = 18]. Da mesma forma, podemos descrever todos os estados em nosso comportamento: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
no último estado [x = 6, y = 6] ambas as partes da expressão serão falsas, então ela não tem próximo estado. Portanto, temos uma especificação completa da segunda etapa - como você pode ver, esta é uma matemática bastante comum, como em engenheiros e cientistas, e não estranha, como em ciência da computação.
Essas duas fórmulas podem ser combinadas em uma fórmula de lógica temporal. Ela é elegante e fácil de explicar, mas não há tempo para ela agora. Podemos precisar de lógica temporal apenas para a propriedade de vivacidade, não é necessária para segurança. Não gosto da lógica temporal como tal, não é uma matemática comum, mas no caso da vivacidade é um mal necessário.
No algoritmo de Euclides, para cada valor x и y tem valores únicos x' и y', que tornam verdadeira a relação com o próximo estado. Em outras palavras, o algoritmo de Euclides é determinístico. Para modelar um algoritmo não determinístico, o estado atual precisa ter vários estados futuros possíveis, e que cada valor de variável não iniciada tenha vários valores de variável iniciada, de modo que a relação com o próximo estado seja verdadeira. Isso é fácil de fazer, mas não darei exemplos agora.
Para fazer uma ferramenta de trabalho, você precisa de matemática formal. Como formalizar a especificação? Para fazer isso, precisamos de uma linguagem formal, por exemplo, . A especificação do algoritmo de Euclides ficaria assim nesta linguagem:
Um símbolo de sinal de igual com um triângulo significa que o valor à esquerda do sinal é definido como igual ao valor à direita do sinal. Em essência, a especificação é uma definição, em nosso caso, duas definições. Para a especificação em TLA+, você precisa adicionar declarações e alguma sintaxe, como no slide acima. Em ASCII ficaria assim:
Como você pode ver, nada complicado. A especificação para TLA+ pode ser testada, ou seja, ignorar todos os comportamentos possíveis em um modelo pequeno. No nosso caso, este modelo terá certos valores M и N. Este é um método de verificação muito eficiente e simples que é totalmente automático. Também é possível escrever provas formais da verdade e verificá-las mecanicamente, mas isso leva muito tempo, então quase ninguém faz isso.
A principal desvantagem do TLA+ é que ele é matemático, e os programadores e cientistas da computação têm medo de matemática. À primeira vista, isso soa como uma piada, mas, infelizmente, falo sério. Meu colega estava me contando como tentou explicar o TLA+ para vários desenvolvedores. Assim que as fórmulas apareceram na tela, eles imediatamente se tornaram olhos vidrados. Portanto, se o TLA+ te assusta, você pode usar , é uma espécie de linguagem de programação de brinquedo. Uma expressão no PlusCal pode ser qualquer expressão TLA+, ou seja, em geral, qualquer expressão matemática. Além disso, PlusCal possui uma sintaxe para algoritmos não determinísticos. Como PlusCal pode escrever qualquer expressão TLA+, PlusCal é muito mais expressivo do que qualquer linguagem de programação real. Em seguida, o PlusCal é compilado em uma especificação TLA+ facilmente legível. Isso não significa, é claro, que a especificação complexa do PlusCal se tornará simples no TLA + - apenas a correspondência entre eles é óbvia, não haverá complexidade adicional. Finalmente, esta especificação pode ser verificada pelas ferramentas TLA+. Em suma, o PlusCal pode ajudar a superar a fobia matemática e é fácil de entender, mesmo para programadores e cientistas da computação. No passado, publiquei algoritmos sobre ele por algum tempo (cerca de 10 anos).
Talvez alguém objete que TLA + e PlusCal são matemática, e matemática só funciona em exemplos inventados. Na prática, você precisa de uma linguagem real com tipos, procedimentos, objetos e assim por diante. Isto está errado. Aqui está o que Chris Newcomb, que trabalhou na Amazon, escreve: “Usamos o TLA+ em dez grandes projetos e, em cada caso, usá-lo fez uma diferença significativa no desenvolvimento porque conseguimos detectar bugs perigosos antes de entrarmos em produção e porque nos deu a visão e a confiança de que precisávamos para fazer otimizações de desempenho agressivas sem afetar a veracidade do programa". Muitas vezes você pode ouvir que, ao usar métodos formais, obtemos um código ineficiente - na prática, tudo é exatamente o oposto. Além disso, existe a opinião de que os gerentes não podem ser convencidos da necessidade de métodos formais, mesmo que os programadores estejam convencidos de sua utilidade. E Newcomb escreve: “Os gerentes agora estão se esforçando para escrever especificações para o TLA + e alocar tempo especificamente para isso”. Portanto, quando os gerentes veem que o TLA+ está funcionando, ficam felizes em aceitá-lo. Chris Newcomb escreveu isso cerca de seis meses atrás (outubro de 2014), mas agora, até onde eu sei, o TLA+ é usado em 14 projetos, não em 10. Outro exemplo está no design do XBox 360. Um estagiário procurou Charles Thacker e escreveu especificação para o sistema de memória. Graças a esta especificação, foi encontrado um bug que de outra forma passaria despercebido e por causa do qual todo XBox 360 travava após quatro horas de uso. Os engenheiros da IBM confirmaram que seus testes não teriam encontrado esse bug.
Você pode ler mais sobre o TLA + na Internet, mas agora vamos falar sobre especificações informais. Raramente precisamos escrever programas que calculam o mínimo divisor comum e coisas do gênero. Com muito mais frequência, escrevemos programas como a ferramenta pretty-printer que escrevi para o TLA+. Após o processamento mais simples, o código TLA + ficaria assim:
Mas no exemplo acima, o usuário provavelmente queria que a conjunção e os sinais de igualdade fossem alinhados. Portanto, a formatação correta ficaria mais ou menos assim:
Considere outro exemplo:
Aqui, ao contrário, o alinhamento dos sinais de igual, adição e multiplicação na fonte era aleatório, portanto, o processamento mais simples é suficiente. Em geral, não existe uma definição matemática exata de formatação correta, pois “correto” neste caso significa “o que o usuário deseja”, e isso não pode ser determinado matematicamente.
Parece que se não tivermos uma definição de verdade, então a especificação é inútil. Mas isso não. Só porque não sabemos o que um programa deve fazer não significa que não precisamos pensar sobre como ele funciona - pelo contrário, temos que nos esforçar ainda mais. A especificação é especialmente importante aqui. É impossível determinar o programa ideal para impressão estruturada, mas isso não significa que não devamos tomá-lo, e escrever código como um fluxo de consciência não é uma coisa boa. No final, escrevi uma especificação de seis regras com definições em forma de comentários em um arquivo java. Aqui está um exemplo de uma das regras: a left-comment token is LeftComment aligned with its covering token. Esta regra está escrita, digamos, em inglês matemático: LeftComment aligned, left-comment и covering token - termos com definições. É assim que os matemáticos descrevem a matemática: eles escrevem definições de termos e, com base neles, regras. O benefício de tal especificação é que seis regras são muito mais fáceis de entender e depurar do que 850 linhas de código. Devo dizer que escrever essas regras não foi fácil, levou muito tempo para depurá-las. Especialmente para esse fim, escrevi um código que informava qual regra foi usada. Graças ao fato de ter testado essas seis regras em vários exemplos, não precisei depurar 850 linhas de código e os bugs acabaram sendo bastante fáceis de encontrar. Java tem ótimas ferramentas para isso. Se eu tivesse apenas escrito o código, levaria muito mais tempo e a formatação seria de pior qualidade.
Por que uma especificação formal não poderia ser usada? Por um lado, a execução correta não é muito importante aqui. Impressões estruturais certamente não agradarão a ninguém, então não precisei fazer com que funcionasse direito em todas as situações estranhas. Mais importante ainda é o fato de eu não ter ferramentas adequadas. O verificador de modelo TLA+ é inútil aqui, então eu teria que escrever manualmente os exemplos.
A especificação acima possui características comuns a todas as especificações. É um nível mais alto que o código. Pode ser implementado em qualquer idioma. Quaisquer ferramentas ou métodos são inúteis para escrevê-lo. Nenhum curso de programação irá ajudá-lo a escrever esta especificação. E não há ferramentas que tornem essa especificação desnecessária, a menos, é claro, que você esteja escrevendo uma linguagem especificamente para escrever programas de impressão estruturada em TLA+. Por fim, essa especificação não diz nada sobre exatamente como escreveremos o código, apenas informa o que o código faz. Escrevemos a especificação para nos ajudar a pensar no problema antes de começarmos a pensar no código.
Mas esta especificação também possui características que a distinguem de outras especificações. 95% das outras especificações são significativamente mais curtas e simples:
Além disso, esta especificação é um conjunto de regras. Como regra, isso é um sinal de especificação ruim. Compreender as consequências de um conjunto de regras é bastante difícil, e é por isso que tive que gastar muito tempo depurando-as. No entanto, neste caso, não consegui encontrar uma maneira melhor.
Vale a pena dizer algumas palavras sobre programas que funcionam continuamente. Via de regra, eles trabalham em paralelo, por exemplo, sistemas operacionais ou sistemas distribuídos. Pouquíssimas pessoas podem entendê-los mentalmente ou no papel, e eu não sou um deles, embora já tenha conseguido fazê-lo. Portanto, precisamos de ferramentas que verifiquem nosso trabalho - por exemplo, TLA + ou PlusCal.
Por que foi necessário escrever uma especificação se eu já sabia exatamente o que o código deveria fazer? Na verdade, eu apenas pensei que sabia. Além disso, com uma especificação, um estranho não precisa mais entrar no código para entender exatamente o que ele faz. Eu tenho uma regra: não deve haver regras gerais. Há uma exceção a essa regra, é claro, é a única regra geral que sigo: a especificação do que o código faz deve dizer às pessoas tudo o que elas precisam saber ao usar o código.
Então, o que exatamente os programadores precisam saber sobre o pensamento? Para começar, o mesmo que todo mundo: se você não escreve, parece que está pensando. Além disso, você precisa pensar antes de codificar, o que significa que precisa escrever antes de codificar. A especificação é o que escrevemos antes de começar a codificar. Uma especificação é necessária para qualquer código que possa ser usado ou modificado por qualquer pessoa. E esse "alguém" pode ser o próprio autor do código um mês depois de ter sido escrito. Uma especificação é necessária para grandes programas e sistemas, para classes, para métodos e, às vezes, até mesmo para seções complexas de um único método. O que exatamente deve ser escrito sobre o código? Você precisa descrever o que ele faz, ou seja, o que pode ser útil para qualquer pessoa que utilize este código. Às vezes também pode ser necessário especificar como o código cumpre seu propósito. Se passamos por esse método no curso de algoritmos, então o chamamos de algoritmo. Se for algo mais especial e novo, chamamos de design de alto nível. Não há diferença formal aqui: ambos são um modelo abstrato de um programa.
Como exatamente você deve escrever uma especificação de código? O principal: deve ser um nível acima do próprio código. Deve descrever estados e comportamentos. Deve ser tão rigoroso quanto a tarefa exige. Se estiver escrevendo uma especificação de como uma tarefa deve ser implementada, você pode escrevê-la em pseudocódigo ou com PlusCal. Você precisa aprender a escrever especificações em especificações formais. Isso lhe dará as habilidades necessárias que também o ajudarão com as informais. Como você aprende a escrever especificações formais? Quando aprendemos a programar, escrevemos programas e depois os depuramos. É o mesmo aqui: escreva a especificação, verifique com o verificador de modelo e corrija os bugs. TLA+ pode não ser a melhor linguagem para uma especificação formal, e outra linguagem provavelmente será melhor para suas necessidades específicas. A vantagem do TLA+ é que ele ensina muito bem o pensamento matemático.
Como vincular especificação e código? Com a ajuda de comentários que ligam conceitos matemáticos e sua implementação. Se você trabalha com gráficos, no nível do programa você terá matrizes de nós e matrizes de links. Portanto, você precisa escrever exatamente como o grafo é implementado por essas estruturas de programação.
Deve-se observar que nenhuma das opções acima se aplica ao processo real de escrever código. Quando você escreve o código, ou seja, executa a terceira etapa, também precisa pensar e pensar no programa. Se uma subtarefa se revelar complexa ou não óbvia, você precisará escrever uma especificação para ela. Mas não estou falando sobre o código em si aqui. Você pode usar qualquer linguagem de programação, qualquer metodologia, não é sobre eles. Além disso, nenhuma das opções acima elimina a necessidade de testar e depurar o código. Mesmo que o modelo abstrato seja escrito corretamente, pode haver bugs em sua implementação.
Escrever especificações é uma etapa adicional no processo de codificação. Graças a ele, muitos erros podem ser detectados com menos esforço - sabemos disso pela experiência dos programadores da Amazon. Com especificações, a qualidade dos programas torna-se maior. Então, por que tantas vezes vamos sem eles? Porque escrever é difícil. E escrever é difícil, porque para isso é preciso pensar, e pensar também é difícil. É sempre mais fácil fingir o que você pensa. Aqui você pode fazer uma analogia com a corrida - quanto menos você corre, mais devagar você corre. Você precisa treinar seus músculos e praticar a escrita. Precisa de prática.
A especificação pode estar incorreta. Você pode ter cometido um erro em algum lugar, ou os requisitos podem ter mudado, ou uma melhoria pode precisar ser feita. Qualquer código que alguém usa deve ser alterado, então, mais cedo ou mais tarde, a especificação não corresponderá mais ao programa. Idealmente, neste caso, você precisa escrever uma nova especificação e reescrever completamente o código. Sabemos muito bem que ninguém faz isso. Na prática, corrigimos o código e possivelmente atualizamos a especificação. Se isso vai acontecer mais cedo ou mais tarde, então por que escrever especificações? Em primeiro lugar, para a pessoa que editará seu código, cada palavra extra na especificação valerá seu peso em ouro, e essa pessoa pode muito bem ser você mesmo. Costumo me repreender por não obter especificações suficientes quando estou editando meu código. E escrevo mais especificações do que código. Portanto, quando você edita o código, a especificação sempre precisa ser atualizada. Em segundo lugar, a cada revisão, o código piora, torna-se cada vez mais difícil de ler e manter. Isso é um aumento na entropia. Mas se você não começar com uma especificação, cada linha que você escrever será uma edição e o código será pesado e difícil de ler desde o início.
Como disse , nenhuma batalha foi vencida por plano, e nenhuma batalha foi vencida sem um plano. E ele sabia uma ou duas coisas sobre batalhas. Há uma opinião de que escrever especificações é uma perda de tempo. Às vezes isso é verdade, e a tarefa é tão simples que não há nada em que pensar. Mas você deve sempre lembrar que, quando lhe dizem para não escrever especificações, é-lhe dito para não pensar. E você deve pensar nisso sempre. Pensar na tarefa não garante que você não cometerá erros. Como sabemos, ninguém inventou a varinha mágica e programar é uma tarefa difícil. Mas se você não pensar no problema, com certeza cometerá erros.
Você pode ler mais sobre TLA + e PlusCal em um site especial, você pode ir lá na minha página inicial . Isso é tudo para mim, obrigado pela atenção.
Por favor, note que esta é uma tradução. Ao escrever comentários, lembre-se de que o autor não os lerá. Se você realmente quiser conversar com o autor, ele estará na conferência Hydra 2019, que será realizada de 11 a 12 de julho de 2019 em São Petersburgo. Os ingressos podem ser adquiridos .
Fonte: habr.com