Este é um artigo de tradução do workshop de Stanford . Mas antes dela é uma pequena introdução. Como os zumbis são formados? Todos caíram em uma situação em que você deseja puxar um amigo ou colega para o seu nível, mas isso não funciona. Além disso, "não dá certo" não tanto para você como para ele: de um lado da balança há um salário normal, tarefas e assim por diante, e do outro - a necessidade de pensar. Pensar é desagradável e doloroso. Ele rapidamente desiste e continua a escrever código, completamente sem incluir o cérebro. Você imagina quanto esforço precisa gastar para superar a barreira do desamparo aprendido e simplesmente não o faz. É assim que os zumbis são formados, que aparentemente podem ser curados, mas parece que ninguém fará isso.
Quando vi que Leslie Lampport (sim, o mesmo amigo dos livros didáticos) estava vindo para a Rússia e não estava dando um relatório, mas uma sessão de perguntas e respostas, fiquei um pouco cauteloso. Apenas para garantir, Leslie é um cientista mundialmente famoso, autor dos trabalhos fundamentais em computação distribuída, e você também pode conhecê-lo pelas letras La no LaTeX - "Lamport TeX". O segundo fator alarmante é sua demanda: todos os que vierem devem (completamente de graça) ouvir antecipadamente alguns de seus relatórios, apresentar pelo menos uma pergunta sobre eles e só então vir. Decidi ver o que Lampport estava transmitindo por lá - e foi ótimo! É exatamente isso, uma pílula mágica para tratar um zumbi. Eu aviso: a partir do texto, pode ser notável que fãs de metodologias super flexíveis e não entusiastas testem o que está escrito.
Depois do habrokat, de fato, começa a tradução do seminário. Boa leitura!
Qualquer que seja a sua tarefa, você sempre precisa seguir três etapas:
- decida qual objetivo você deseja alcançar;
- decida como você alcançará seu objetivo;
- chegar ao seu objetivo.
Isso também se aplica à programação. Quando escrevemos o código, precisamos:
- decidir o que o programa deve fazer;
- determinar exatamente como deve cumprir sua tarefa;
- escreva o código apropriado.
O último passo, é claro, é muito importante, mas não vou falar sobre isso hoje. Em vez disso, discutimos os dois primeiros. Cada programador os executa antes de começar a trabalhar. Você não se senta para escrever se ainda não decidiu o que está escrevendo: um navegador ou um banco de dados. Uma ideia definitiva do objetivo deve estar presente. E você tem certeza de pensar sobre o que exatamente o programa fará e não escrever de alguma forma, na esperança de que o próprio código se torne um navegador.
Como exatamente esse pensamento preliminar do código ocorre? Quanto esforço devemos gastar nisso? Tudo depende de quão difícil é o problema que estamos resolvendo. Suponha que desejemos escrever um sistema distribuído tolerante a falhas. Nesse caso, devemos considerar tudo corretamente antes de nos sentarmos para o código. E se precisarmos apenas aumentar a variável inteira em 1? À primeira vista, tudo é trivial aqui, e não são necessários pensamentos, mas depois lembramos que o estouro pode ocorrer. Portanto, mesmo para entender se um problema é simples ou complexo, você primeiro precisa pensar.
Se você pensar em possíveis soluções para o problema, 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 Gindon: "Quando você escreve, a natureza mostra como seu pensamento é desleixado". Se você não escreve, apenas parece que você pensa. E você precisa anotar seus pensamentos na forma de especificações.
As especificações cumprem muitas funções, especialmente em grandes projetos. Mas falarei 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? Esta é sempre sempre a primeira pergunta para os programadores: em que idioma vamos escrever. Não há uma resposta correta: os problemas que resolvemos são muito diversos. O TLA + é útil para alguns - essa é a linguagem de especificação que eu desenvolvi. Para outros, é mais conveniente usar chinês. Tudo depende da situação.
Outra questão é mais importante: como alcançar um pensamento mais claro? Resposta: devemos pensar como cientistas. Essa é uma maneira de pensar que se provou nos ú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. Este modelo, como qualquer outro, foi projetado para resolver certos problemas. É ótimo para determinar para onde apontar o telescópio, se você precisar encontrar um planeta. Mas se você quiser prever o clima neste planeta, este 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, ciência da computação. A realidade com a qual trabalhamos é computar sistemas de vários tipos: processadores, consoles de jogos, computadores, programas em execução e assim por diante. Vou falar sobre a execução de um programa em um computador, mas, em geral, todas essas conclusões se aplicam a qualquer sistema de computador. Em nossa ciência, usamos muitos modelos diferentes: uma máquina de Turing, conjuntos de eventos parcialmente encomendados 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 apresentação do programa para o usuário, depois escrevemos um esquema de alto nível do programa e, finalmente, escrevemos o código. Enquanto escrevemos o código, entendemos que precisamos escrever uma ferramenta para formatar o texto. Aqui, novamente, precisamos resolver três problemas: determinar qual texto essa ferramenta retornará; escolha um algoritmo para formatação; escreva código. Esta tarefa possui sua própria subtarefa: insira hífens nas palavras corretamente. Também resolvemos essa subtarefa em três etapas - como vemos, 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 fornece alguma saída. Em matemática, uma função é geralmente descrita como um conjunto ordenado de pares. Por exemplo, a função quadrática para números naturais é descrita como o conjunto {<0,0>, <1,1>, <2,4>, <3,9>, ...}. O escopo dessa função é o conjunto dos primeiros elementos de cada par, ou seja, 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 as mesmas que funções em linguagens de programação. A matemática é muito mais simples. Como não tenho tempo para exemplos complexos, considere 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 deste método, escrevemos: 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 é divisível por M e N Como a realidade se relaciona com esse modelo? O modelo opera com números inteiros e, em C ou Java, temos um int 32 bits. Esse modelo nos permite decidir se o algoritmo GCD está correto, 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 da função como modelo. O trabalho de alguns programas (por exemplo, sistemas operacionais) não se resume ao retorno de um certo valor para certos argumentos; eles podem ser executados continuamente. Além disso, a função como modelo não é adequada para o segundo passo: planejar um método para resolver o problema. A classificação rápida e a classificação de bolhas calculam a mesma função, mas esses são algoritmos completamente diferentes. Portanto, para descrever a maneira de atingir a meta do programa, eu uso um modelo diferente, vamos chamá-lo de modelo comportamental padrão. O programa é apresentado como o conjunto de todos os comportamentos permitidos, cada um dos quais, por sua vez, é uma sequência de estados e um estado é uma atribuição de valores a variáveis.
Vamos ver como será o segundo passo para o algoritmo euclidiano. Precisamos calcular o GCD(M, N) . Inicializamos M como x , e N como y , e sub-subtraímos a menor dessas variáveis da maior até que 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 ? O zero é divisível por todos os números; portanto, não existe um maior divisor nesse caso. Nessa situação, precisamos retornar à primeira etapa e perguntar: realmente precisamos calcular o MDC para números não positivos? Se isso não for necessário, basta alterar a especificação.
Uma pequena digressão sobre produtividade deve ser feita aqui. 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 erros. E a maneira mais fácil de se livrar do código é na primeira etapa. É 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 valem a pena. O segundo passo está em segundo lugar em termos de potencial para economizar tempo. Se você medir a produtividade pelo número de linhas escritas, pensar em como concluir a tarefa o tornará menos produtivo , pois você pode resolver o mesmo problema com menos código. Não posso fornecer estatísticas exatas aqui, porque não tenho como calcular o número de linhas que não escrevi porque passei algum tempo na especificação, ou seja, na primeira e na segunda etapas. E o experimento também não pode ser colocado aqui, porque no experimento não temos o direito de concluir o primeiro passo, a tarefa é predeterminada.
Nas especificações informais, muitas dificuldades são facilmente ignoradas. Não há nada complicado ao escrever especificações estritas para funções, não discutirei isso. Em vez disso, falaremos sobre escrever especificações rigorosas para modelos comportamentais padrão. Existe um teorema que afirma que qualquer conjunto de comportamentos pode ser descrito usando a propriedade de segurança e a propriedade liveness . Segurança significa que nada de ruim vai acontecer, o programa não dará a resposta errada. Vitalidade significa que mais cedo ou mais tarde algo bom acontecerá, isto é, o programa dará mais cedo ou mais tarde a resposta correta. Como regra, a segurança é um indicador mais importante; os erros costumam surgir aqui. Portanto, para economizar tempo, não falarei sobre capacidade de sobrevivência, embora, é claro, também seja importante.
Alcançamos segurança prescrevendo, em primeiro lugar, os muitos possíveis estados iniciais. E segundo, os relacionamentos com todos os possíveis próximos estados para cada estado. Nos comportaremos como cientistas e definiremos os estados matematicamente. O conjunto de estados iniciais é descrito pela fórmula, por exemplo, no caso do algoritmo euclidiano: (x = M) ∧ (y = N) . Para certos valores de M e N existe apenas um estado inicial. O relacionamento com o próximo estado é descrito por uma fórmula na qual as variáveis do próximo estado são gravadas com um hífen e o estado atual sem um hífen. No caso do algoritmo euclidiano, trataremos da disjunção de duas fórmulas, em uma das quais x é o maior valor e na segunda - y :
No primeiro caso, o novo valor de y é igual ao valor anterior de y, e obtemos o novo valor de x, subtraindo o menor da variável maior. No segundo caso, fazemos o oposto.
Vamos voltar ao algoritmo euclidiano. Suponha novamente que M = 12 , N = 18 . Isso determina o ú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 possui um próximo estado. Portanto, temos a especificação completa do segundo passo - como vemos, isso é matemática bastante comum, como a de engenheiros e cientistas, e não estranha, como na ciência da computação.
Essas duas fórmulas podem ser combinadas em uma fórmula lógica temporal. Ela é elegante e fácil de explicar, mas agora não tem tempo. Podemos precisar de lógica temporal apenas para a propriedade de vivacidade, pois segurança não é necessária. A lógica temporal, como tal, não é agradável, não é matemática comum, mas, no caso da vivacidade, é um mal necessário.
No algoritmo euclidiano, para cada valor de x e y existem valores únicos de x' e y' que tornam verdadeira a relação com o próximo estado. Em outras palavras, o algoritmo euclidiano é determinístico. Para simular um algoritmo não determinístico, é necessário que o estado atual possua vários estados futuros possíveis e que cada valor da variável sem primo tenha vários valores da variável com um toque no qual a relação com o próximo estado seja verdadeira. Isso não é difícil de fazer, mas não vou dar 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, TLA + . A especificação do algoritmo euclidiano nesta linguagem terá a seguinte aparência:
O símbolo do 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, uma especificação é uma definição, no nosso caso duas definições. Você precisa adicionar declarações e alguma sintaxe à especificação no TLA +, como no slide acima. No ASCII, será assim:
Como você pode ver, nada complicado. A especificação do TLA + pode ser verificada, ou seja, ignora todos os comportamentos possíveis em um modelo pequeno. No nosso caso, este modelo terá certos valores de M e N Este é um método de verificação muito eficiente e fácil que é executado automaticamente. Além disso, você pode escrever provas formais da verdade e verificá-las mecanicamente, mas isso leva muito tempo, então quase ninguém o faz.
A principal desvantagem do TLA + é que é matemática, e programadores e cientistas da computação têm medo da matemática. À primeira vista, isso soa como uma piada, mas, infelizmente, digo isso com toda a seriedade. Meu colega acabou de me contar como ele tentou explicar o TLA + para vários desenvolvedores. Assim que as fórmulas apareceram na tela, eles imediatamente tiveram olhos de vidro. Portanto, se o TLA + é assustador, você pode usar o PlusCal , é um tipo de linguagem de programação de brinquedos. Uma expressão no PlusCal pode ser qualquer expressão TLA +, ou seja, em geral, qualquer expressão matemática. O PlusCal também possui sintaxe para algoritmos não determinísticos. Devido ao fato de que qualquer expressão TLA + pode ser escrita no PlusCal, é muito mais expressiva que qualquer linguagem de programação real. O PlusCal é ainda mais compilado na especificação TLA + de fácil leitura. Isso não significa, é claro, que a especificação PlusCal complexa se torne simples no TLA + - apenas a correspondência entre elas é óbvia, não haverá complexidade adicional. Finalmente, essa especificação pode ser verificada com as ferramentas TLA +. Em geral, o PlusCal pode ajudar a superar a fobia da matemática; é fácil entender, mesmo para programadores e cientistas da computação. No passado, por algum tempo (cerca de 10 anos), publiquei algoritmos nele.
Talvez alguém objete que TLA + e PlusCal são matemática, e a matemática funciona apenas em exemplos inventados. Na prática, você precisa de uma linguagem real com tipos, procedimentos, objetos e assim por diante. Isto não é verdade. Aqui está o que Chris Newcomb, que trabalhou na Amazon, escreve: “Usamos o TLA + em dez grandes projetos e, em cada caso, seu uso contribuiu significativamente para o desenvolvimento, porque conseguimos capturar bugs perigosos antes de entrar em produção e porque ele nos deu compreensão e confiança necessárias para otimizações de desempenho agressivas que não afetam a verdade do programa " . Você pode ouvir muitas vezes que, ao usar métodos formais, obtemos um código ineficiente - na prática, tudo é exatamente o oposto. Além disso, acredita-se que os gerentes não possam ser convencidos da necessidade de métodos formais, mesmo que os programadores estejam convencidos de sua utilidade. E Newcomb escreve: "Agora, os gerentes estão se esforçando em todos os aspectos para escrever especificações para o TLA +, e dedicam especificamente tempo 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 (em outubro de 2014), mas agora, tanto quanto eu sei, o TLA + é usado em 14 projetos, não em 10. Outro exemplo está relacionado ao design do XBox 360. Um estagiário veio a Charles Thacker e escreveu especificação para um sistema de memória. Graças a essa especificação, foi encontrado um bug que, de outra forma, não teria sido percebido e, por causa disso, cada XBox 360 cairia após quatro horas de uso. Os engenheiros da IBM confirmaram que seus testes não teriam detectado esse bug.
Você pode ler mais sobre o TLA + na Internet e agora vamos falar sobre especificações informais. Raramente precisamos escrever programas que computem o divisor menos comum e similares. Com mais freqüência, escrevemos programas como a ferramenta de impressora bonita 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 igual fossem alinhados. Portanto, a formatação correta seria mais parecida com esta:
Considere outro exemplo:
Aqui, pelo contrário, o alinhamento de sinais de igual, adição e multiplicação na fonte foi aleatório, portanto o processamento mais simples é suficiente. Em geral, não existe uma definição matemática exata da formatação correta, porque "correto" neste caso significa "o que o usuário deseja" e isso não pode ser matematicamente determinado.
Parece que, se não tivermos uma definição de verdade, a especificação será inútil. Mas isso não é verdade. Se não sabemos exatamente o que o programa deve fazer, isso não significa que não precisamos refletir sobre o seu trabalho - pelo contrário, devemos dedicar ainda mais esforços a isso. A especificação aqui é especialmente importante. É impossível determinar o programa ideal para a listagem estrutural, mas isso não significa que não devamos realizá-lo, e escrever código como um fluxo de consciência não é uma coisa. No final, escrevi uma especificação de seis regras com definições na 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 em, digamos, em inglês matemático: LeftComment aligned , left-comment e covering token são termos com definições. É assim que os matemáticos descrevem a matemática: eles escrevem definições de termos e com base nelas - regras. O benefício desta especificação é que entender e depurar as seis regras é muito mais simples que 850 linhas de código. Devo dizer que escrever essas regras não foi fácil, muito tempo foi gasto na depuração delas. Especialmente para esse fim, escrevi um código que informava qual regra era usada. Devido ao fato de eu ter verificado essas seis regras com alguns exemplos, não precisei depurar 850 linhas de código, e os bugs se mostraram bastante fáceis de encontrar. Java tem ótimas ferramentas para isso. Se eu apenas escrevesse o código, levaria muito mais tempo e a formatação acabaria sendo de pior qualidade.
Por que era impossível usar uma especificação formal? Por um lado, a execução correta não é muito importante aqui. Uma listagem estrutural certamente não agradará ninguém, por isso não precisei obter o trabalho certo em todas as situações incomuns. Ainda mais importante é o fato de eu não ter ferramentas adequadas. A ferramenta para testar os modelos TLA + é inútil aqui, então eu teria que escrever exemplos manualmente.
A especificação fornecida possui recursos comuns a todas as especificações. É de um nível superior ao código. Você pode implementá-lo em qualquer idioma. Para escrevê-lo, quaisquer ferramentas ou métodos são inúteis. Nenhum curso de programação o ajudará a escrever essa especificação. E não há ferramentas que possam tornar essa especificação desnecessária, a menos que, é claro, você escreva uma linguagem específica para escrever programas de listagem estrutural no TLA +. Finalmente, esta especificação não diz nada sobre exatamente como escreveremos o código, apenas indica o que esse código faz. Estamos escrevendo uma especificação para nos ajudar a refletir sobre o problema antes de começarmos a pensar em código.
Mas essa especificação também possui recursos que a distinguem de outras especificações. 95% de outras especificações são muito mais curtas e simples:
Além disso, esta especificação é um conjunto de regras. Isso geralmente é um sinal de baixa especificação. Compreender as implicações do 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. Como regra, eles trabalham em paralelo, por exemplo, sistemas operacionais ou sistemas distribuídos. Muito poucos conseguem entendê-los em suas mentes ou no papel, e eu não sou um deles, embora eu pudesse pagar. Portanto, são necessárias ferramentas que testarão nosso trabalho - por exemplo, TLA + ou PlusCal.
Por que você precisou escrever uma especificação se eu já sabia o que exatamente o código deveria fazer? De fato, parecia-me que eu sabia disso. Além disso, se houver uma especificação, um estranho não precisará mais entrar no código para entender o que exatamente ele está fazendo. Eu tenho uma regra: não deve haver nenhuma regra geral. Essa regra, é claro, tem uma exceção, esta é a única regra geral que sigo: a especificação do que o código faz é dizer à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 iniciantes, o mesmo que todos: se você não escreve, então pensa apenas que pensa. Além disso, você precisa pensar antes de codificar, o que significa que você precisa escrever antes de codificar. Uma especificação é o que escrevemos antes de começarmos a codificar. A especificação é necessária para qualquer código que possa ser usado ou modificado por qualquer pessoa. E esse "alguém" pode se tornar o autor do código um mês depois de escrevê-lo. A especificação é necessária para grandes programas e sistemas, classes, métodos e, às vezes, até seções complexas de um único método. O que exatamente precisa ser escrito sobre o código? É necessário descrever o que ele está fazendo, isto é, algo que pode ser útil para qualquer pessoa que use esse código. Às vezes, também pode ser necessário indicar exatamente como o código atinge seu objetivo. Se passamos esse método no curso de algoritmos, chamamos de algoritmo. Se é algo mais especial e novo, chamamos de design de alto nível. Não há diferença formal: ambos são um modelo abstrato do programa.
Como exatamente uma especificação de código deve ser escrita? O principal: deve ser um nível superior ao código em si. Deve descrever estados e comportamentos. Deve ser tão rigoroso quanto a tarefa exige. Se você estiver escrevendo uma especificação de como implementar a tarefa, ela poderá ser escrita em pseudo-código ou usando o PlusCal. Aprender a escrever especificações é necessário em especificações formais. Isso lhe dará as habilidades necessárias que ajudarão a incluir as pessoas informais. E como aprender a escrever especificações formais? Quando aprendemos a programação, escrevemos programas e os depuramos. : , . TLA+, , , . TLA+ , .
? , . , . , .
, . , , . , . . , , . , . , .
— . — Amazon. . ? . , , . , . — , . . .
. - , , . , - , , . . , . , , . , ? -, , , , . , . , . , , . -, , . . , , .
, , . - . , — . , , . , , , , . . , . , , — . , .
TLA+ PlusCal , . , .
, . — , . , Hydra 2019, 11-12 2019 -. .