Este é um artigo de tradução . Mas antes, uma breve introdução. Como se formam zumbis? Todos já se encontraram na situação de querer ajudar um amigo ou colega a evoluir profissionalmente, mas não conseguiram. E não é tanto você o problema, mas sim ele: de um lado está um salário razoável, tarefas, e assim por diante, e do outro lado está a necessidade de pensar. Pensar é desagradável e doloroso. Ele desiste rapidamente e continua escrevendo código, sem usar o cérebro. Você consegue imaginar quanto esforço é necessário para superar a barreira da impotência aprendida e simplesmente não faz isso. Assim se formam zumbis que, aparentemente, podem ser curados, mas que, de fato, ninguém se disporá a tratar.
Quando eu vi que (sim, aquele mesmo das aulas) e não fará uma palestra, mas sim uma sessão de perguntas e respostas, eu fiquei um pouco apreensivo. Para seu conhecimento, Leslie é um cientista de renome mundial, autor de trabalho fundamental em computação distribuída, e você pode conhecê-lo pelas letras La na palavra LaTeX — "Lamport TeX". Um fator que aumentou minha apreensão é sua exigência: todos que comparecerem devem (totalmente de graça) ouvir algumas de suas palestras antecipadamente, formular pelo menos uma pergunta sobre elas e somente assim comparecer. Decidi ver o que Lamport tinha a dizer — e é maravilhoso! É exatamente a coisa, uma mágica superlink que funciona como remédio para a zumbificação. Aviso: aqueles que amam metodologias excessivamente flexíveis e detestam testar o que escrevem podem se sentir ofendidos com o texto.
Após essa introdução, começa a tradução do seminário. Boa leitura!
Independentemente da tarefa que você escolher, você sempre precisa passar por três etapas:
- definir qual objetivo você deseja alcançar;
- decidir como exatamente você irá alcançar seu objetivo;
- chegar ao seu objetivo.
Isso também se aplica à programação. Quando escrevemos código, precisamos:
- decidir o que exatamente o programa deve fazer;
- definir como deve executar sua tarefa;
- escrever o código correspondente.
O último passo é, sem dúvida, muito importante, mas não vou falar sobre ele hoje. Em vez disso, vamos discutir os dois primeiros. Cada programador os realiza antes de começar a trabalhar. Você não começa a escrever se não decidiu o que exatamente está escrevendo: um navegador ou um banco de dados. É essencial ter uma noção clara do objetivo. E você deve pensar no que exatamente o programa fará, em vez de escrever de qualquer jeito esperando que o código se torne um navegador por conta própria.
Como exatamente acontece esse planejamento prévio do código? Quanto esforço devemos dedicar a isso? Tudo depende da complexidade do problema que estamos resolvendo. Suponha que queremos escrever um sistema distribuído à prova de falhas. Nesse caso, devemos pensar em tudo cuidadosamente antes de começar a codificar. E se precisarmos apenas incrementar uma variável inteira em 1? À primeira vista, parece trivial, e não é necessário refletir, mas depois nos lembramos que pode ocorrer um estouro. Portanto, mesmo para entender se um problema é simples ou complexo, primeiro precisamos pensar.
Se você planejar com antecedência possíveis soluções para o problema, pode evitar erros. Mas para isso, é necessário que seu pensamento esteja claro. Para alcançar isso, é preciso registrar seus pensamentos. Eu gosto muito da citação de Dick Hinton: "Quando você escreve, a natureza lhe mostra quão desleixado é seu pensamento". Se você não escreve, apenas parece que está pensando. E é necessário registrar seus pensamentos na forma de especificações.
As especificações desempenham muitas funções, especialmente em projetos grandes. Mas vou falar apenas sobre uma delas: elas nos ajudam a pensar com clareza. Pensar com clareza é muito importante e bastante difícil, portanto, precisamos de qualquer suporte nesse aspecto. Em qual língua devemos escrever as especificações? Essa é sempre a primeira pergunta para os programadores: em que idioma vamos escrever. Não há uma resposta correta única: os problemas que resolvemos são muito variados. Para alguns, o TLA+ é útil — é a linguagem de especificações que desenvolvi. Para outros, é mais conveniente usar o chinês. Tudo depende da situação.
Mas importante é a outra questão: como alcançar um pensamento mais claro? A resposta: devemos pensar como cientistas. Este é um modo de pensar que se comprovou eficaz nos últimos 500 anos. Na ciência, construímos modelos matemáticos da realidade. A astronomia foi, sem dúvida, a primeira ciência a ser considerada rigorosamente. 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 fluxos. Este modelo, como qualquer outro, foi criado para resolver tarefas específicas. Ele é muito bom para determinar onde direcionar o telescópio quando se procura um planeta. Mas se você quiser prever o clima naquele planeta, esse modelo não servirá.
A matemática nos permite definir 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 executando programas e assim por diante. Farei uma discussão sobre a execução de um programa em um computador, mas, em essência, todas essas conclusões se aplicam a qualquer sistema computacional. 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? É qualquer código que pode ser considerado de forma independente. Suponha que precisamos escrever um navegador. Executamos três tarefas: projetamos a apresentação do programa para o usuário, depois escrevemos um esboço de alto nível do programa e, finalmente, escrevemos o código. Ao longo da escrita do código, percebemos que precisamos criar uma ferramenta para formatação de texto. Aqui, novamente, precisamos resolver três tarefas: definir qual texto essa ferramenta irá retornar; escolher um algoritmo para formatação; escrever o código. Esta tarefa tem uma subtarefa: inserir corretamente o hífen nas palavras. Nós também resolvemos essa subtarefa em três passos — como podemos ver, eles se repetem em muitos níveis.
Vamos analisar mais detalhadamente o primeiro passo: qual problema o programa resolve. Aqui, frequentemente modelamos o programa como uma função que recebe certos dados de entrada e fornece alguns dados de saída. Na matemática, a função é geralmente descrita como um conjunto ordenado de pares. Por exemplo, a função de elevar ao quadrado para números naturais é descrita como o conjunto {, , , , ...}. O domínio dessa função é o conjunto dos primeiros elementos de cada par, ou seja, os números naturais. Para definir a função, precisamos especificar seu domínio e a fórmula.
Mas funções na matemática não são o mesmo que funções em linguagens de programação. A matemática é significativamente mais simples. 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 maior divisor comum de dois números inteiros. Na especificação desse método, escreveremos: calcula GCD(M,N) para os argumentos M e N, onde GCD(M,N) — uma função, cujo domínio é o conjunto de pares de números inteiros, e o valor de retorno é o maior número inteiro que divide M e N. Como esse modelo se relaciona com a realidade? O modelo opera com números inteiros, enquanto em C ou Java temos um int32 bits. Esse modelo nos permite determinar se o algoritmo é correto GCD, mas não evita erros de estouro. Para isso, seria necessário um modelo mais complexo, para o qual não há tempo.
Vamos falar sobre as limitações da função como modelo. O funcionamento de alguns programas (por exemplo, sistemas operacionais) não se limita a retornar um valor específico para argumentos específicos; eles podem ser executados continuamente. Além disso, a função como modelo não se adapta bem ao segundo passo: o planejamento de como resolver o problema. A ordenação rápida e a ordenação por bolhas calculam a mesma função, mas são algoritmos completamente diferentes. Portanto, para descrever a maneira de alcançar o objetivo do programa, utilizo um modelo diferente, que chamaremos de modelo comportamental padrão. Neste modelo, o programa é representado como um conjunto de todos os comportamentos permitidos, cada um dos quais, por sua vez, é uma sequência de estados, e um estado é a atribuição de valores a variáveis.
Vamos ver como será o segundo passo para o algoritmo de Euclides. Precisamos calcular MDC(M, N). Inicializamos M como x, e N como y, em seguida, subtraímos repetidamente o menor desses valores do maior até que eles sejam iguais. Por exemplo, se M = 12, e N = 18, podemos descrever o seguinte comportamento:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
E se M = 0 e N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Aqui, é importante fazer uma breve pausa sobre produtividade. Ela é frequentemente medida pelo número de linhas de código escritas por dia. Mas seu trabalho é muito mais valioso se você eliminou um certo número de linhas, pois isso reduz o espaço para bugs. E é mais fácil eliminar código exatamente na primeira etapa. É bastante possível que você simplesmente não precise de todas aquelas complexidades que está tentando implementar. A maneira mais rápida de simplificar um programa e economizar tempo é não fazer coisas que não valem a pena ser feitas. O segundo passo é o segundo em potencial para economia de tempo. Se você mede a produtividade pelo número de linhas escritas, o planejamento de como executar a tarefa tornará você menos produtivo, uma vez que você poderá resolver a mesma tarefa com menos linhas de código. Não posso fornecer estatísticas exatas aqui, pois não tenho como contar quantas linhas não escrevi graças ao tempo que gastei na especificação, ou seja, nos primeiro e segundo passos. E também não se pode realizar um experimento aqui, porque em um experimento não temos o direito de realizar o primeiro passo, a tarefa é definida com antecedência.
Nas especificações informais, é fácil esquecer muitas dificuldades. Não há nada complicado em escrever especificações rigorosas para funções, não discutirei isso. Em vez disso, falaremos sobre como escrever especificações rigorosas para modelos de comportamento padrão. Existe um teorema que diz que qualquer conjunto de comportamentos pode ser descrito usando a propriedade de segurança (safety) e a propriedade de vivacidade (liveness)A segurança significa que nada de ruim acontecerá, o programa não fornecerá uma resposta incorreta. A vitalidade significa que, cedo ou tarde, algo bom acontecerá, ou seja, o programa, cedo ou tarde, dará a resposta correta. Geralmente, a segurança é um indicador mais importante, os erros ocorrem mais frequentemente aqui. Portanto, para economizar tempo, não vou falar sobre vitalidade, embora, é claro, isso também seja importante.
Nós alcançamos segurança descrevendo, em primeiro lugar, uma infinidade de estados iniciais possíveis. E, em segundo lugar, as relações com todos os possíveis estados subsequentes para cada estado. Vamos agir como cientistas e definir os 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 e 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 um acento, enquanto as do estado atual são escritas sem acento. No caso do algoritmo de Euclides, lidaremos com a disjunção de duas fórmulas, uma das quais x é o maior valor, e a outra é y:
No primeiro caso, o novo valor de y é igual ao valor anterior de y, e o novo valor de x obtemos subtraindo a variável menor da maior. No segundo caso, fazemos o contrário.
Voltemos ao algoritmo de Euclides. Suponhamos novamente que M = 12, N = 18. Isso define um único estado inicial, (x = 12) ∧ (y = 18). Em seguida, substituímos esses valores na fórmula acima e obtemos:
Aqui, a única solução possível é: x' = 18 - 12 ∧ y' = 12, e 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, portanto, não há próximo estado. Assim, temos a especificação completa do segundo passo — como vemos, isso é uma matemática bastante comum, como a dos engenheiros e cientistas, e não estranha, como na ciência da computação.
Essas duas fórmulas podem ser combinadas em uma única fórmula de lógica temporal. Ela é elegante e não é difícil de explicar, mas não há tempo para isso agora. A lógica temporal pode ser necessária apenas para a propriedade de vivacidade; para segurança, não é necessária. A lógica temporal, em si, não é agradável, não é matemática completamente comum, mas, no caso da vivacidade, é um mal necessário.
No algoritmo de Euclides, para cada valor x e y existem valores únicos x' e y', que tornam a relação com o próximo estado verdadeira. Em outras palavras, o algoritmo de Euclides é determinístico. Para modelar um algoritmo não determinístico, é necessário que o estado atual tenha vários estados futuros possíveis e que cada valor da variável sem acento tenha vários valores da variável com acento, nos quais a relação com o próximo estado é verdadeira. Isso não é complicado de fazer, mas não irei apresentar exemplos agora.
Para criar uma ferramenta funcional, é necessária matemática formal. Como tornar uma especificação formal? Para isso, precisaremos de uma linguagem formal, como . A especificação do algoritmo de Euclides nesse idioma seria apresentada da seguinte forma:
O símbolo do sinal de igualdade com um triângulo significa que o valor à esquerda do sinal é definido como igual ao valor à direita do sinal. Essencialmente, a especificação é uma definição, no nosso caso, duas definições. À especificação em TLA+ é necessário adicionar declarações e alguma sintaxe, como mostrado no slide acima. Em ASCII, isso seria representado assim:
Como podemos ver, nada complicado. A especificação em TLA+ pode ser validada, ou seja, percorrer todos os comportamentos possíveis em um pequeno modelo. No nosso caso, esse modelo será valores definidos. M e NEsse é um método muito eficaz e simples de verificação, que é inteiramente realizado de forma automática. Além disso, é possível escrever provas formais de veracidade e verificá-las mecanicamente, mas isso leva muito tempo, então quase ninguém faz isso.
A principal desvantagem do TLA+ é que se trata de matemática, e programadores e cientistas da computação têm receio da matemática. À primeira vista, isso soa como uma piada, mas, infelizmente, eu falo isso muito a sério. Meu colega acabou de me contar como tentou explicar o TLA+ a alguns desenvolvedores. Assim que fórmulas apareceram na tela, seus olhos ficaram imediatamente vidrados. Portanto, se o TLA+ assusta, pode-se usar , que é uma espécie de linguagem de programação simplificada. Uma expressão em PlusCal pode ser qualquer expressão TLA+, ou seja, na sua essência, qualquer expressão matemática. Além disso, o PlusCal possui uma sintaxe para algoritmos não determinísticos. Por permitir a escrita de qualquer expressão TLA+, é significativamente mais expressivo do que qualquer linguagem de programação real. Em seguida, PlusCal é compilado em uma especificação TLA+ de fácil leitura. Isso não significa, claro, que uma especificação complicada em PlusCal se tornará simples em TLA+ — apenas a correspondência entre elas é evidente, não surgirá complexidade adicional. Finalmente, essa especificação pode ser verificada com ferramentas TLA+. Em resumo, o PlusCal pode ajudar a superar o medo da matemática, sendo fácil de entender até mesmo para programadores e cientistas da computação. No passado, por algum tempo (cerca de 10 anos), publiquei algoritmos nessa linguagem.
Pode ser que alguém argumente que TLA+ e PlusCal são matemática, e que a matemática só funciona em exemplos inventados. Na prática, um verdadeiro idioma com tipos, procedimentos, objetos e assim por diante é necessário. Isso não é verdade. Veja o que diz Chris Newcomb, que trabalhou na Amazon: “Usamos TLA+ em dez grandes projetos, e em cada caso seu uso trouxe uma contribuição significativa para o desenvolvimento, porque conseguimos identificar bugs perigosos antes de chegarem à produção, e porque nos deu o entendimento e a confiança necessários para otimizações de desempenho agressivas, sem afetar a veracidade do programa”. Frequentemente se ouve que, com métodos formais, obtemos código ineficaz — na prática, porém, é exatamente o oposto. Além disso, há a crença de que é impossível convencer gerentes da necessidade de métodos formais, mesmo que os programadores estejam convencidos de sua utilidade. E Newcomb escreve: Os gerentes agora estão cada vez mais incentivando a elaboração de especificações em TLA+, e dedicam tempo para isso.Portanto, quando os gerentes percebem que o TLA+ funciona, eles o aceitam com entusiasmo. Chris Newcomb escreveu isso há cerca de seis meses (em outubro de 2014), e agora, pelo que sei, o TLA+ está sendo usado em 14 projetos, e não 10. Outro exemplo se refere ao design do XBox 360. Charles Thacker recebeu um estagiário que escreveu uma especificação para o sistema de memória. Graças a essa especificação, um bug foi identificado, que de outra forma não seria notado, e que faria com que cada XBox 360 travasse após quatro horas de uso. Engenheiros da IBM confirmaram que seus testes não teriam detectado esse bug.
Você pode ler mais sobre TLA+ na internet, mas agora vamos falar sobre especificações informais. Raramente precisamos escrever programas que calculam o maior divisor comum e coisas assim. Muito mais frequentemente, escrevemos programas como uma ferramenta de impressão estruturada (pretty-printer), que eu desenvolvi para TLA+. Após o processamento mais simples, o código em TLA+ pareceria o seguinte:
Mas, no exemplo dado, o usuário provavelmente desejava que os operadores de conjunção e igualdade estivessem alinhados. Portanto, a formatação correta seria mais assim:
Vamos considerar outro exemplo:
Aqui, por outro lado, o alinhamento dos sinais de igualdade, adição e multiplicação na fonte era aleatório, então o processamento mais simples é totalmente suficiente. Em geral, não há uma definição matemática precisa do que é a formatação correta, porque 'correto' aqui significa 'como o usuário quer', e isso não pode ser definido matematicamente.
À primeira vista, se não temos uma definição de verdade, a especificação parece inútil. Mas não é. Se não sabemos exatamente o que o programa deve fazer, isso não significa que não devemos pensar sobre seu funcionamento — ao contrário, devemos dedicar ainda mais esforços a isso. A especificação é especialmente importante aqui. Definir o programa ideal para impressão estruturada é impossível, mas isso não significa que não devemos tentar, e escrever código como um fluxo de consciência não é o caminho. No final, eu escrevi uma especificação de seis regras com definições na forma de comentários. no arquivo Java. Aqui está um exemplo de uma das regras: um token de comentário à esquerda é LeftComment alinhado com seu token de cobertura. Esta regra está escrita em, digamos, inglês matemático: LeftComment alinhado, comentário à esquerda e token de cobertura — termos com definições. É assim que os matemáticos descrevem a matemática: escrevem definições de termos e com base nelas — regras. A vantagem de tal especulação é que entender e depurar seis regras é significativamente mais fácil do que 850 linhas de código. É preciso dizer que escrever essas regras não foi fácil, levou bastante tempo para depurá-las. Especialmente para este objetivo, escrevi um código que indicava qual regra estava sendo usada. Graças ao fato de que testei essas seis regras em vários exemplos, não precisei depurar 850 linhas de código, e os bugs se mostraram bastante fáceis de encontrar. No Java, existem ótimas ferramentas para isso. Se eu tivesse apenas escrito o código, teria levado muito mais tempo, e a formatação seria de qualidade inferior.
Por que não foi possível usar uma especificação formal? Por um lado, a correção aqui não é tão importante. A impressão estrutural com certeza desagrada alguém, então eu não precisava garantir o bom funcionamento em todas as situações não convencionais. Mais importante ainda, eu não tinha ferramentas adequadas. A ferramenta de verificação de modelos TLA+ é inútil aqui, então eu teria que escrever os exemplos manualmente.
A especificação apresentada tem características comuns a todas as especificações. Ela é de um nível mais alto do que o código. Pode ser implementada em qualquer linguagem. Para escrevê-la, quaisquer ferramentas ou métodos são inúteis. Nenhum curso de programação ajudará você a escrever esta especificação. E não existem ferramentas que poderiam tornar essa especificação desnecessária, a não ser que você esteja escrevendo uma linguagem especificamente para escrever programas de impressão estrutural em TLA+. Finalmente, essa especificação não diz nada sobre como exatamente vamos escrever o código, ela apenas indica o que esse código faz. Escrevemos uma especificação para nos ajudar a pensar sobre o problema antes de começarmos a pensar no código.
Mas essa especificação tem características que a distinguem de outras especificações. 95% das outras especificações são significativamente mais curtas e mais simples:
Além disso, esta especificação é um conjunto de regras. Em geral, isso é um sinal de uma má especificação. Compreender as consequências de um conjunto de regras pode ser bastante difícil, e é exatamente por isso que tive que gastar muito tempo depurando-as. No entanto, neste caso, não consegui encontrar uma melhor maneira.
Vale a pena mencionar algumas palavras sobre os programas que funcionam continuamente. Em geral, eles operam em paralelo, como sistemas operacionais ou sistemas distribuídos. Poucas pessoas conseguem entendê-los na mente ou no papel, e eu não sou uma delas, embora já tenha conseguido isso um dia. Portanto, são necessárias ferramentas que verifiquem nosso trabalho — por exemplo, TLA+ ou PlusCal.
Por que escrever uma especificação se eu já sabia o que o código deveria fazer? Na verdade, eu apenas pensava que sabia. Além disso, com uma especificação, uma pessoa de fora não precisa mais se aprofundar no código para entender o que ele faz. Eu tenho uma regra: não deve haver regras gerais. É claro que essa regra tem uma exceção, que é a única regra geral que sigo: a especificação do que o código faz deve informar às pessoas tudo o que elas precisam saber ao usar esse código.
Então, o que exatamente os programadores precisam saber sobre o pensamento? Para começar, o mesmo que todos: se você não escreve, parece que está pensando. Além disso, é preciso pensar antes de codificar, o que significa que você deve escrever antes de codificar. A especificação é o que escrevemos antes de começar a codificar. A especificação é necessária para qualquer código que possa ser utilizado ou modificado por alguém. E esse "alguém" pode ser o próprio autor do código um mês após a sua criação. A especificação é necessária para grandes programas e sistemas, para classes, para métodos e, às vezes, até mesmo para trechos complexos de um único método. O que exatamente deve ser escrito sobre o código? Deve-se descrever o que ele faz, isto é, o que pode ser útil para qualquer pessoa que use esse código. Às vezes, pode ser necessário indicar como o código atinge seu objetivo. Se essa abordagem foi discutida no curso de algoritmos, chamamos isso de algoritmo. Se for algo mais específico e novo, chamamos de design de alto nível. Não há diferença formal aqui: ambos são modelos abstratos de programa.
Como exatamente devemos escrever uma especificação de código? O principal: ela deve estar um nível acima do próprio código. Ela deve descrever estados e comportamentos. Ela deve ser tão rigorosa quanto a tarefa exige. Se você está escrevendo uma especificação para a implementação de uma tarefa, ela pode ser escrita em pseudocódigo ou usando PlusCal. Aprender a escrever especificações deve ser feito com especificações formais. Isso lhe dará as habilidades necessárias que ajudarão também com as não formais. E como aprender a escrever especificações formais? Quando aprendemos programação, escrevíamos programas e depois os depurávamos. O mesmo se aplica aqui: você precisa escrever uma especificação, testá-la usando uma ferramenta de verificação de modelos e corrigir erros. TLA+ pode não ser a melhor linguagem para especificações formais, e para suas necessidades específicas outra linguagem provavelmente será mais adequada. A vantagem do TLA+ é que ele ensina bem o pensamento matemático.
Como vincular a especificação e o código? Através de comentários que conectam conceitos matemáticos à sua implementação. Se você estiver trabalhando com grafos, então em nível de programa você terá arrays de nós e arrays de conexões. Portanto, você precisa escrever como exatamente o grafo é implementado por essas estruturas de programação.
É importante notar que nada do que foi dito acima se relaciona ao próprio processo de escrita de código. Quando você escreve código, ou seja, quando executa a terceira etapa, você também precisa pensar e refinar o programa. Se uma sub-tarefa se mostrar complicada ou não óbvia, é necessário escrever uma especificação para ela. Mas não estou falando do código em si. Você pode usar qualquer linguagem de programação, qualquer metodologia, isso não é o foco. Além disso, nada do que foi dito até agora elimina a necessidade de testar e depurar o código. Mesmo que o modelo abstrato seja escrito corretamente, a sua implementação pode conter bugs.
A escrita de especificações é uma etapa adicional no processo de escrita de código. Graças a ela, muitos erros podem ser capturados com menos esforço — isso sabemos pela experiência de programadores da Amazon. Com especificações, a qualidade dos programas aumenta. Então, por que frequentemente conseguimos fazer isso sem elas? Porque escrever é difícil. E escrever é difícil porque é preciso pensar, e pensar também é difícil. Sempre é mais fácil fingir que está pensando. Aqui, podemos traçar uma analogia com a corrida — quanto menos você corre, mais devagar você vai. É necessário treinar seus músculos e praticar a escrita. A prática é fundamental.
A especificação pode estar errada. Você pode ter cometido um erro em algum lugar, ou os requisitos podem ter mudado, ou uma melhoria pode ter se tornado necessária. Qualquer código que alguém usa acaba precisando ser alterado, portanto, mais cedo ou mais tarde, a especificação deixará de corresponder ao programa. Idealmente, nesse caso, seria necessário escrever uma nova especificação e reescrever o código completamente. Sabemos que praticamente ninguém faz isso. Na prática, nós fazemos patches no código e, talvez, atualizamos a especificação. Se isso deve acontecer mais cedo ou mais tarde, então por que escrever especificações? Em primeiro lugar, para a pessoa que vai editar seu código, cada palavra extra na especificação será valiosa, e essa pessoa pode muito bem ser você mesmo. Costumo me criticar pela falta de especificação ao editar meu código. E eu escrevo mais especificações do que código. Portanto, ao editar o código, a especificação deve sempre ser atualizada. Em segundo lugar, a cada edição, o código se torna pior, fica cada vez mais difícil de ler e manter. Isso é um aumento de entropia. Mas se você não começa com uma especificação, cada linha escrita será uma edição, e o código desde o início será volumoso e difícil de ler.
Como disse , , nenhuma batalha foi vencida de acordo com o plano, e nenhuma batalha foi vencida sem um plano.E ele sabia algo sobre batalhas. Existe a opinião de que escrever especificações é uma perda de tempo. Às vezes, realmente é, e a tarefa é tão simples que não há nada a considerar. Mas sempre lembre-se de que, quando lhe dizem para não escrever especificações, isso significa que estão lhe aconselhando a não pensar. E isso é algo a se considerar a cada vez. Pensar na tarefa não garante que você não cometerá erros. Como sabemos, ninguém inventou uma varinha mágica, e programar é uma atividade complexa. Mas se você não pensa na tarefa, você garante que cometerá erros.
Para saber mais sobre TLA+ e PlusCal, você pode visitar o site especial, que pode ser acessado a partir da minha página inicial. Isso é tudo por agora, obrigado pela atenção.
Lembro que isso é uma tradução. Ao escrever comentários, lembre-se de que o autor não os lerá. Se você realmente deseja se comunicar com o autor, ele estará na conferência Hydra 2019, que ocorrerá de 11 a 12 de julho de 2019 em São Petersburgo. Os ingressos podem ser adquiridos .
Fonte: habr.com
