프로그래밍은 코딩 그 이상이다

이 글은 번역본입니다 스탠포드 세미나. 그러나 그녀의 작은 소개 전에. 좀비는 어떻게 형성됩니까? 누구나 친구나 동료를 자신의 수준으로 끌어올리고 싶은데 잘 되지 않는 상황에 처한다. 그리고 "작동하지 않는다"는 것은 당신과 함께하는 것이 아닙니다. 저울의 한쪽에는 정상적인 급여, 작업 등이 있고 다른쪽에는 생각할 필요가 있습니다. 생각하는 것은 불쾌하고 고통스럽습니다. 그는 재빨리 포기하고 뇌를 전혀 켜지 않은 채 코드 작성을 계속합니다. 학습된 무력감의 장벽을 극복하는 데 얼마나 많은 노력이 필요한지 상상하고는 하지 않습니다. 이것이 좀비가 형성되는 방식으로 치료할 수있는 것 같지만 아무도하지 않는 것 같습니다.

내가 그것을 보았을 때 레슬리 램포트 (예, 교과서의 같은 동지) 러시아에 온다 보고서를 작성하지 않고 질의 응답 시간에 조금 조심했습니다. 만일을 대비하여 Leslie는 세계적으로 유명한 과학자이자 분산 컴퓨팅의 기본 작업의 저자이며 LaTeX- "Lamport TeX"라는 단어의 La 문자로도 그를 알 수 있습니다. 두 번째 놀라운 요소는 그의 요구 사항입니다. 오는 모든 사람은 (절대 무료로) 사전에 그의 보고서 몇 가지를 듣고 적어도 하나의 질문을 한 다음에만 와야합니다. 나는 Lamport가 그곳에서 무엇을 방송하고 있는지 보기로 결정했습니다. 바로 그 것, 좀비를 치료하는 마법의 연결 알약입니다. 나는 당신에게 경고합니다 : 텍스트에서 매우 유연한 방법론을 좋아하고 작성된 것을 테스트하는 것을 좋아하지 않는 사람들은 눈에 띄게 소진 될 수 있습니다.

habrokat 이후 실제로 세미나 번역이 시작됩니다. 독서를 즐기십시오!

어떤 작업을 수행하든 항상 다음 세 단계를 거쳐야 합니다.

• 달성하려는 목표를 결정하십시오.
• 목표를 달성하는 방법을 결정합니다.
• 당신의 목표에 오십시오.

이것은 프로그래밍에도 적용됩니다. 코드를 작성할 때 다음을 수행해야 합니다.

• 프로그램이 무엇을 해야 하는지 결정합니다.
• 작업을 수행하는 방법을 결정합니다.
• 해당 코드를 작성하십시오.

물론 마지막 단계는 매우 중요하지만 오늘은 그것에 대해 이야기하지 않겠습니다. 대신 처음 두 가지에 대해 설명하겠습니다. 모든 프로그래머는 작업을 시작하기 전에 수행합니다. 브라우저를 작성할지 데이터베이스를 작성할지 결정하지 않는 한 글을 쓰기 위해 앉지 않습니다. 목표에 대한 특정 아이디어가 있어야합니다. 그리고 프로그램이 정확히 무엇을 할 것인지 확실히 생각하고 코드가 어떻게 든 브라우저로 바뀔 것이라는 희망으로 어떻게 든 작성하지 마십시오.

이 코드 사전 사고는 정확히 어떻게 발생합니까? 여기에 얼마나 많은 노력을 기울여야 할까요? 그것은 모두 우리가 해결하고 있는 문제가 얼마나 복잡한가에 달려 있습니다. 내결함성 분산 시스템을 작성한다고 가정합니다. 이 경우 코드를 작성하기 전에 신중하게 생각해야 합니다. 정수 변수를 1씩 증가시키면 어떻게 됩니까? 언뜻 보기에 여기에서는 모든 것이 사소하고 생각할 필요가 없지만 오버플로가 발생할 수 있음을 기억합니다. 따라서 문제가 단순한지 복잡한지 이해하기 위해서라도 먼저 생각할 필요가 있습니다.

문제에 대한 가능한 해결책을 미리 생각하면 실수를 피할 수 있습니다. 그러나 이렇게 하려면 생각이 명확해야 합니다. 이를 달성하려면 생각을 적어야 합니다. 나는 Dick Guindon의 인용문을 정말 좋아합니다. "글을 쓸 때 자연은 당신의 생각이 얼마나 엉성한지 보여줍니다." 글을 쓰지 않으면 생각하고 있다고 생각할 뿐입니다. 그리고 당신의 생각을 명세의 형태로 적어야 합니다.

사양은 특히 대규모 프로젝트에서 많은 기능을 수행합니다. 그러나 나는 그 중 한 가지에 대해서만 이야기할 것입니다. 그것들은 우리가 명확하게 생각하도록 도와줍니다. 명확하게 생각하는 것은 매우 중요하고 매우 어렵기 때문에 여기에서 도움이 필요합니다. 어떤 언어로 사양을 작성해야 합니까? 일반적으로 이것은 프로그래머에게 항상 첫 번째 질문입니다. 어떤 언어로 작성할 것인지입니다. 이에 대한 정답은 없습니다. 우리가 해결하고 있는 문제는 너무 다양합니다. 누군가에게 TLA+는 내가 개발한 사양 언어입니다. 다른 사람들에게는 중국어를 사용하는 것이 더 편리합니다. 모든 것은 상황에 달려 있습니다.

더 중요한 것은 또 다른 질문입니다. 더 명확한 사고를 달성하는 방법은 무엇입니까? 대답: 우리는 과학자처럼 생각해야 합니다. 이것은 지난 500년 동안 입증된 사고 방식입니다. 과학에서 우리는 현실의 수학적 모델을 구축합니다. 천문학은 아마도 엄밀한 의미에서 최초의 과학이었을 것입니다. 천문학에서 사용되는 수학적 모델에서 천체는 질량, 위치 및 운동량을 가진 점으로 나타나지만 실제로는 산과 바다, 조수와 조수를 가진 매우 복잡한 물체입니다. 이 모델은 다른 것과 마찬가지로 특정 문제를 해결하기 위해 만들어졌습니다. 행성을 찾아야 하는 경우 망원경이 가리키는 위치를 결정하는 데 유용합니다. 하지만 이 행성의 날씨를 예측하고 싶다면 이 모델은 작동하지 않을 것입니다.

수학을 통해 모델의 속성을 결정할 수 있습니다. 그리고 과학은 이러한 속성이 현실과 어떻게 관련되는지 보여줍니다. 우리의 과학, 컴퓨터 과학에 대해 이야기해 봅시다. 우리가 작업하는 현실은 프로세서, 게임 콘솔, 컴퓨터, 프로그램 실행 등 다양한 종류의 컴퓨팅 시스템입니다. 컴퓨터에서 프로그램을 실행하는 것에 대해 이야기하겠지만 대체로 이러한 모든 결론은 모든 컴퓨팅 시스템에 적용됩니다. 우리 과학에서는 튜링 기계, 부분적으로 정렬된 이벤트 세트 등 다양한 모델을 사용합니다.

프로그램이란 무엇입니까? 이것은 독립적으로 간주할 수 있는 모든 코드입니다. 브라우저를 작성해야 한다고 가정합니다. 우리는 세 가지 작업을 수행합니다. 프로그램에 대한 사용자 관점을 디자인한 다음 프로그램의 상위 수준 다이어그램을 작성하고 마지막으로 코드를 작성합니다. 코드를 작성하면서 텍스트 포맷터를 작성해야 한다는 것을 깨달았습니다. 여기서 다시 세 가지 문제를 해결해야 합니다. 이 도구가 반환할 텍스트를 결정합니다. 포맷 알고리즘을 선택하십시오. 코드를 작성합니다. 이 작업에는 자체 하위 작업이 있습니다. 단어에 하이픈을 올바르게 삽입하십시오. 또한 이 하위 작업을 세 단계로 해결합니다. 보시다시피 여러 단계에서 반복됩니다.

첫 번째 단계인 프로그램이 해결하는 문제를 더 자세히 살펴보겠습니다. 여기에서 우리는 프로그램을 일부 입력을 받고 일부 출력을 생성하는 함수로 가장 자주 모델링합니다. 수학에서 함수는 일반적으로 쌍의 순서 집합으로 설명됩니다. 예를 들어, 자연수에 대한 제곱 함수는 {<0,0>, <1,1>, <2,4>, <3,9>, …} 집합으로 설명됩니다. 이러한 함수의 도메인은 각 쌍의 첫 번째 요소 집합, 즉 자연수입니다. 함수를 정의하려면 범위와 공식을 지정해야 합니다.

그러나 수학의 함수는 프로그래밍 언어의 함수와 같지 않습니다. 수학이 훨씬 쉽습니다. 복잡한 예제를 할 시간이 없기 때문에 간단한 예제를 살펴보겠습니다. C의 함수 또는 두 정수의 최대 공약수를 반환하는 Java의 정적 메서드입니다. 이 방법의 사양에서 다음과 같이 작성합니다. GCD(M,N) 인수 M и N어디에서 GCD(M,N) - 도메인이 정수 쌍의 집합이고 반환 값이 다음으로 나눌 수 있는 가장 큰 정수인 함수 M и N. 이 모델은 현실과 어떤 관련이 있습니까? 모델은 정수에서 작동하지만 C 또는 Java에서는 32비트 int. 이 모델을 사용하면 알고리즘이 올바른지 결정할 수 있습니다. GCD, 그러나 오버플로 오류를 방지하지는 않습니다. 이를 위해서는 시간이 없는 보다 복잡한 모델이 필요합니다.

모델로서의 함수의 한계에 대해 이야기해 봅시다. 일부 프로그램(예: 운영 체제)은 특정 인수에 대해 특정 값을 반환할 뿐 아니라 계속 실행할 수 있습니다. 또한 모델로서의 기능은 문제 해결 방법을 계획하는 두 번째 단계에 적합하지 않습니다. 퀵 정렬과 버블 정렬은 같은 함수를 계산하지만 완전히 다른 알고리즘입니다. 따라서 프로그램의 목표가 어떻게 달성되는지 설명하기 위해 다른 모델을 사용합니다. 이를 표준 행동 모델이라고 하겠습니다. 그 안의 프로그램은 허용 가능한 모든 행동의 집합으로 표현되며, 각각은 일련의 상태이며 상태는 변수에 값을 할당하는 것입니다.

Euclid 알고리즘의 두 번째 단계가 어떻게 생겼는지 봅시다. 우리는 계산해야합니다 GCD(M, N). 초기화한다 M как x과 N как y그런 다음 두 변수가 같아질 때까지 더 큰 변수에서 더 작은 변수를 반복해서 뺍니다. 예를 들어, M = 12과 N = 18, 다음 동작을 설명할 수 있습니다.

[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]

그리고 만약 M = 0 и N = 0? XNUMX은 모든 숫자로 나눌 수 있으므로 이 경우에는 최대 약수가 없습니다. 이 상황에서 우리는 첫 번째 단계로 돌아가서 다음과 같이 질문해야 합니다. 양수가 아닌 숫자에 대해 GCD를 계산해야 합니까? 이것이 필요하지 않은 경우 사양을 변경하기만 하면 됩니다.

여기서 우리는 생산성에 대해 약간의 여담을 가져야 합니다. 하루에 작성되는 코드 줄 수로 측정되는 경우가 많습니다. 그러나 버그의 여지가 적기 때문에 특정 수의 줄을 제거하면 작업이 훨씬 더 유용합니다. 코드를 제거하는 가장 쉬운 방법은 첫 번째 단계입니다. 구현하려는 모든 종소리와 휘파람이 필요하지 않을 수도 있습니다. 프로그램을 단순화하고 시간을 절약하는 가장 빠른 방법은 하지 말아야 할 일을 하지 않는 것입니다. 두 번째 단계는 두 번째로 시간을 가장 많이 절약할 수 있는 잠재력입니다. 작성된 줄의 관점에서 생산성을 측정하면 작업을 수행하는 방법에 대해 생각하면 덜 생산적, 더 적은 코드로 동일한 문제를 해결할 수 있기 때문입니다. 스펙, 즉 첫 번째 단계와 두 번째 단계에 시간을 할애하여 작성하지 않은 줄 수를 셀 방법이 없기 때문에 여기서 정확한 통계를 제공할 수 없습니다. 그리고 여기에서도 실험을 설정할 수 없습니다. 실험에서 우리는 첫 번째 단계를 완료할 권리가 없기 때문에 작업이 미리 결정됩니다.

비공식 사양의 많은 어려움을 간과하기 쉽습니다. 함수에 대한 엄격한 사양을 작성하는 데 어려운 것은 없으며 이에 대해서는 논의하지 않겠습니다. 대신 표준 동작에 대한 강력한 사양을 작성하는 방법에 대해 이야기하겠습니다. 보안 속성을 사용하여 모든 동작 집합을 설명할 수 있다는 정리가 있습니다. (안전) 및 생존 속성 (생생함). 보안은 나쁜 일이 발생하지 않으며 프로그램이 잘못된 답변을 제공하지 않음을 의미합니다. 생존 가능성은 조만간 좋은 일이 일어날 것임을 의미합니다. 즉, 프로그램이 조만간 정답을 제공할 것입니다. 일반적으로 보안이 더 중요한 지표이며 여기에서 오류가 가장 자주 발생합니다. 따라서 시간을 절약하기 위해 물론 생존 가능성도 중요하지만 생존 가능성에 대해 이야기하지 않겠습니다.

먼저 가능한 초기 상태 집합을 규정하여 보안을 달성합니다. 둘째, 각 상태에 대해 가능한 모든 다음 상태와의 관계입니다. 과학자처럼 행동하고 상태를 수학적으로 정의해 봅시다. 초기 상태 집합은 예를 들어 Euclid 알고리즘의 경우 공식으로 설명됩니다. (x = M) ∧ (y = N). 특정 값의 경우 M и N 초기 상태는 하나뿐입니다. 다음 상태와의 관계는 다음 상태의 변수는 소수로 쓰고 현재 상태의 변수는 소수 없이 쓰는 공식으로 설명됩니다. 유클리드 알고리즘의 경우 두 공식의 분리를 다룰 것입니다. x 가장 큰 값이고 두 번째 - y:

첫 번째 경우 y의 새 값은 이전 y 값과 같고 더 큰 변수에서 더 작은 변수를 빼서 새 x 값을 얻습니다. 두 번째 경우에는 그 반대입니다.

유클리드의 알고리즘으로 돌아가 봅시다. 다시 가정해보자 M = 12, N = 18. 이것은 단일 초기 상태를 정의합니다. (x = 12) ∧ (y = 18). 그런 다음 해당 값을 위의 공식에 연결하고 다음을 얻습니다.

가능한 유일한 해결책은 다음과 같습니다. x' = 18 - 12 ∧ y' = 12그리고 우리는 행동을 얻습니다: [x = 12, y = 18]. 마찬가지로 행동의 모든 상태를 설명할 수 있습니다. [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].

마지막 상태에서 [x = 6, y = 6] 식의 두 부분이 모두 거짓이므로 다음 상태가 없습니다. 그래서 우리는 두 번째 단계에 대한 완전한 사양을 가지고 있습니다. 보시다시피 이것은 엔지니어와 과학자와 같은 매우 일반적인 수학이며 컴퓨터 과학과 같이 이상하지 않습니다.

이 두 공식은 시간 논리의 하나의 공식으로 결합될 수 있습니다. 그녀는 우아하고 설명하기 쉽지만 지금은 시간이 없습니다. 우리는 활성 속성에 대해서만 임시 논리가 필요할 수 있으며 보안에는 필요하지 않습니다. 나는 그런 시간 논리를 좋아하지 않습니다. 그것은 평범한 수학이 아니지만 생동감의 경우에는 필요악입니다.

유클리드 알고리즘에서 각 값에 대해 x и y 고유한 값을 갖는다 x' и y', 다음 상태와의 관계를 참으로 만듭니다. 즉, 유클리드의 알고리즘은 결정론적입니다. 비결정론적 알고리즘을 모델링하기 위해서는 현재 상태가 여러 개의 가능한 미래 상태를 가질 필요가 있고, 각각의 비결정 변수 값은 다음 상태와의 관계가 참이 되도록 여러 프라임 변수 값을 가져야 합니다. 이것은 하기 쉽지만 지금은 예를 제시하지 않겠습니다.

작업 도구를 만들려면 공식 수학이 필요합니다. 사양을 공식화하는 방법은 무엇입니까? 이를 위해서는 공식 언어가 필요합니다. 예를 들면 다음과 같습니다. TLA+. Euclid 알고리즘의 사양은 이 언어에서 다음과 같습니다.

삼각형이 있는 등호 기호는 기호 왼쪽의 값이 기호 오른쪽의 값과 동일하게 정의됨을 의미합니다. 본질적으로 사양은 정의이며 우리의 경우 두 가지 정의입니다. TLA+의 사양에 위의 슬라이드와 같이 선언과 일부 구문을 추가해야 합니다. ASCII에서는 다음과 같습니다.

보시다시피 복잡한 것은 없습니다. TLA+에 대한 사양을 테스트할 수 있습니다. 즉, 작은 모델에서 가능한 모든 동작을 우회합니다. 우리의 경우 이 모델은 특정 값이 될 것입니다. M и N. 이는 완전히 자동으로 수행되는 매우 효율적이고 간단한 검증 방법입니다. 공식적인 진실 증명을 작성하고 기계적으로 확인하는 것도 가능하지만 시간이 많이 걸리므로 거의 수행하지 않습니다.

TLA+의 가장 큰 단점은 그것이 수학이고 프로그래머와 컴퓨터 과학자들이 수학을 두려워한다는 것입니다. 언뜻 보면 농담처럼 들리지만 불행히도 진심으로 말하는 것입니다. 내 동료는 그가 여러 개발자에게 TLA+를 어떻게 설명하려고 했는지 말해주었습니다. 공식이 화면에 나타나자 금세 눈시울이 붉어졌다. 따라서 TLA+가 두렵다면 다음을 사용할 수 있습니다. 플러스칼, 일종의 장난감 프로그래밍 언어입니다. PlusCal의 식은 모든 TLA+ 식, 즉 대체로 모든 수학적 식일 수 있습니다. 또한 PlusCal에는 비결정적 알고리즘에 대한 구문이 있습니다. PlusCal은 모든 TLA+ 표현식을 작성할 수 있기 때문에 PlusCal은 실제 프로그래밍 언어보다 훨씬 표현력이 뛰어납니다. 다음으로 PlusCal은 쉽게 읽을 수 있는 TLA+ 사양으로 컴파일됩니다. 물론 이것은 복잡한 PlusCal 사양이 TLA +에서 단순한 사양으로 바뀔 것이라는 의미는 아닙니다. 그들 사이의 대응이 분명하고 추가 복잡성이 없을 것입니다. 마지막으로 이 사양은 TLA+ 도구로 확인할 수 있습니다. 대체로 PlusCal은 수학 공포증을 극복하는 데 도움이 될 수 있으며 프로그래머와 컴퓨터 과학자도 쉽게 이해할 수 있습니다. 과거에는 한동안(약 10년) 알고리즘을 게시했습니다.

아마도 누군가는 TLA +와 PlusCal이 수학이고 수학은 발명된 예에서만 작동한다고 반대할 것입니다. 실제로는 유형, 프로시저, 객체 등이 포함된 실제 언어가 필요합니다. 이것은 잘못된 것입니다. 다음은 Amazon에서 근무한 Chris Newcomb이 작성한 내용입니다. “우리는 XNUMX개의 주요 프로젝트에서 TLA+를 사용해 왔으며, 생산에 들어가기 전에 위험한 버그를 포착할 수 있었고 우리에게 프로그램의 진실성에 영향을 미치지 않으면서 공격적인 성능 최적화를 수행합니다.". 공식적인 방법을 사용할 때 비효율적인 코드가 생성된다는 말을 자주 듣습니다. 실제로는 모든 것이 정반대입니다. 또한 프로그래머가 유용성을 확신하더라도 관리자는 형식적 방법의 필요성을 확신할 수 없다는 의견이 있습니다. 그리고 Newcomb은 다음과 같이 씁니다. "관리자들은 이제 TLA+에 대한 사양을 작성하고 특히 이를 위한 시간을 할당하기 위해 열심히 노력하고 있습니다.". 따라서 관리자는 TLA+가 작동하는 것을 보면 기꺼이 받아들입니다. Chris Newcomb이 이 글을 쓴 것은 약 2014개월 전(14년 10월)이지만 지금은 내가 아는 한 TLA+가 360개가 아닌 360개의 프로젝트에서 사용되고 있습니다. 또 다른 예는 XBox XNUMX의 디자인과 관련이 있습니다. 메모리 시스템에 대한 사양을 작성했습니다. 이 사양 덕분에 다른 방법으로는 눈에 띄지 않고 모든 XBox XNUMX이 XNUMX시간 사용 후 충돌하는 버그가 발견되었습니다. IBM 엔지니어는 테스트에서 이 버그를 발견하지 못했음을 확인했습니다.

인터넷에서 TLA +에 대한 자세한 내용을 읽을 수 있지만 이제 비공식 사양에 대해 이야기하겠습니다. 우리는 최소 공약수 등을 계산하는 프로그램을 작성할 필요가 거의 없습니다. 훨씬 더 자주 우리는 TLA+용으로 작성한 예쁜 프린터 도구와 같은 프로그램을 작성합니다. 가장 간단한 처리 후 TLA + 코드는 다음과 같습니다.

그러나 위의 예에서 사용자는 접속사와 등호가 정렬되기를 원했을 가능성이 높습니다. 따라서 올바른 형식은 다음과 같습니다.

다른 예를 생각해보십시오.

여기서 반대로 소스의 등호, 덧셈, 곱셈 기호의 정렬은 무작위이므로 가장 간단한 처리만으로도 충분합니다. 일반적으로 올바른 서식에 대한 정확한 수학적 정의는 없습니다. 이 경우 "올바른"은 "사용자가 원하는 것"을 의미하고 이는 수학적으로 결정할 수 없기 때문입니다.

진리에 대한 정의가 없다면 명세는 쓸모가 없는 것 같습니다. 하지만 그렇지 않습니다. 프로그램이 무엇을 해야 하는지 모른다고 해서 프로그램이 어떻게 작동하는지 생각할 필요가 없는 것은 아닙니다. 오히려 프로그램에 더 많은 노력을 기울여야 합니다. 여기에서 사양이 특히 중요합니다. 구조화된 인쇄를 위한 최적의 프로그램을 결정하는 것은 불가능하지만, 그렇다고 해서 아예 받아들이지 말아야 한다는 의미는 아니며, 의식의 흐름대로 코드를 작성하는 것은 좋지 않습니다. 결국 정의가 있는 XNUMX가지 규칙의 사양을 작성했습니다. 댓글 형식으로 자바 파일에서. 다음은 규칙 중 하나의 예입니다. a left-comment token is LeftComment aligned with its covering token. 이 규칙은 수학 영어로 작성됩니다. LeftComment aligned, left-comment и covering token - 정의가 있는 용어. 이것은 수학자들이 수학을 설명하는 방법입니다. 그들은 용어의 정의를 작성하고 이를 기반으로 규칙을 작성합니다. 이러한 사양의 이점은 850개의 규칙이 850줄의 코드보다 훨씬 이해하고 디버그하기 쉽다는 것입니다. 이 규칙을 작성하는 것이 쉽지 않았고 디버깅하는 데 꽤 많은 시간이 걸렸습니다. 특히 이를 위해 어떤 규칙이 사용되었는지 보고하는 코드를 작성했습니다. 여러 예제에서 이 XNUMX가지 규칙을 테스트한 덕분에 XNUMX줄의 코드를 디버깅할 필요가 없었고 버그를 찾기가 매우 쉬웠습니다. Java에는 이를 위한 훌륭한 도구가 있습니다. 방금 코드를 작성했다면 시간이 훨씬 더 오래 걸렸을 것이고 형식화의 품질도 좋지 않았을 것입니다.

공식 사양을 사용할 수 없는 이유는 무엇입니까? 한편으로 올바른 실행은 여기에서 그다지 중요하지 않습니다. 구조적 인쇄물은 누구도 만족시키지 못할 수밖에 없었기 때문에 모든 이상한 상황에서 제대로 작동하도록 할 필요가 없었습니다. 더 중요한 것은 적절한 도구가 없다는 사실입니다. TLA+ 모델 검사기는 여기서 쓸모가 없으므로 수동으로 예제를 작성해야 합니다.

위의 사양은 모든 사양에 공통되는 기능이 있습니다. 코드보다 높은 수준입니다. 모든 언어로 구현할 수 있습니다. 어떤 도구나 방법도 쓸 수 없습니다. 어떤 프로그래밍 과정도 이 사양을 작성하는 데 도움이 되지 않습니다. 물론 TLA+에서 구조화된 인쇄 프로그램을 작성하기 위해 특별히 언어를 작성하지 않는 한 이 사양을 불필요하게 만들 수 있는 도구는 없습니다. 마지막으로, 이 명세는 우리가 코드를 작성하는 방법에 대해 정확히 언급하지 않고 코드가 수행하는 작업만 설명합니다. 우리는 코드에 대해 생각하기 전에 문제를 충분히 생각하는 데 도움이 되도록 사양을 작성합니다.

그러나이 사양에는 다른 사양과 구별되는 기능도 있습니다. 다른 사양의 95%는 훨씬 더 짧고 간단합니다.

또한 이 사양은 일련의 규칙입니다. 일반적으로 이것은 사양이 좋지 않다는 신호입니다. 일련의 규칙의 결과를 이해하는 것은 매우 어렵기 때문에 규칙을 디버깅하는 데 많은 시간을 할애해야 했습니다. 그러나 이 경우 더 나은 방법을 찾지 못했습니다.

지속적으로 실행되는 프로그램에 대해 몇 마디 말할 가치가 있습니다. 일반적으로 운영 체제 또는 분산 시스템과 같이 병렬로 작동합니다. 정신적으로나 종이로 이해할 수있는 사람은 거의 없으며 한때는 할 수 있었지만 나는 그들 중 하나가 아닙니다. 따라서 TLA + 또는 PlusCal과 같이 작업을 확인할 도구가 필요합니다.

코드가 정확히 무엇을 해야 하는지 이미 알고 있는데 사양을 작성해야 하는 이유는 무엇입니까? 사실 나만 아는 줄 알았다. 또한 사양이 있으면 외부인이 자신이 정확히 무엇을 하는지 이해하기 위해 더 이상 코드에 들어갈 필요가 없습니다. 규칙이 있습니다. 일반적인 규칙은 없어야 합니다. 물론 이 규칙에는 예외가 있습니다. 제가 따르는 유일한 일반적인 규칙입니다. 코드가 수행하는 작업에 대한 사양은 사람들이 코드를 사용할 때 알아야 할 모든 것을 알려야 합니다.

그렇다면 프로그래머는 사고에 대해 정확히 무엇을 알아야 할까요? 우선, 다른 모든 사람과 동일합니다. 글을 쓰지 않으면 생각하고있는 것 같습니다. 또한 코딩하기 전에 생각해야 합니다. 즉, 코딩하기 전에 작성해야 합니다. 사양은 코딩을 시작하기 전에 작성하는 것입니다. 누구나 사용하거나 수정할 수 있는 코드에는 사양이 필요합니다. 그리고 이 "누군가"는 코드가 작성된 지 한 달 후에 코드를 작성한 사람일 수 있습니다. 대형 프로그램 및 시스템, 클래스, 메소드, 때로는 단일 메소드의 복잡한 섹션에 대한 사양이 필요합니다. 코드에 대해 정확히 무엇을 작성해야 합니까? 그것이 무엇을 하는지, 즉 이 코드를 사용하는 사람에게 무엇이 유용할 수 있는지 설명해야 합니다. 경우에 따라 코드가 목적을 달성하는 방법을 지정해야 할 수도 있습니다. 알고리즘의 과정에서 이 방법을 거쳤다면 이를 알고리즘이라고 합니다. 좀 더 특별하고 새로운 것이라면 고급 디자인이라고 합니다. 여기에는 공식적인 차이점이 없습니다. 둘 다 프로그램의 추상 모델입니다.

코드 사양을 정확히 어떻게 작성해야 합니까? 가장 중요한 것은 코드 자체보다 한 단계 더 높아야 한다는 것입니다. 상태와 동작을 설명해야 합니다. 작업이 요구하는 만큼 엄격해야 합니다. 작업 구현 방법에 대한 사양을 작성하는 경우 유사 코드 또는 PlusCal로 작성할 수 있습니다. 정식 사양에 사양을 작성하는 방법을 배워야 합니다. 이것은 비공식적인 것에도 도움이 될 필요한 기술을 제공할 것입니다. 공식 사양을 작성하는 방법을 어떻게 배우나요? 프로그래밍을 배웠을 때 우리는 프로그램을 작성한 다음 디버깅했습니다. 여기서도 마찬가지입니다. 사양을 작성하고 모델 검사기로 확인하고 버그를 수정합니다. TLA+는 공식 사양에 가장 적합한 언어가 아닐 수 있으며 특정 요구 사항에는 다른 언어가 더 나을 수 있습니다. TLA+의 장점은 수학적 사고를 아주 잘 가르친다는 것입니다.

사양과 코드를 연결하는 방법은 무엇입니까? 수학적 개념과 구현을 연결하는 주석의 도움으로. 그래프로 작업하는 경우 프로그램 수준에서 노드 배열과 링크 배열을 갖게 됩니다. 따라서 이러한 프로그래밍 구조에 의해 그래프가 구현되는 방식을 정확하게 작성해야 합니다.

위의 어느 것도 실제 코드 작성 프로세스에는 적용되지 않는다는 점에 유의해야 합니다. 코드를 작성할 때, 즉 세 번째 단계를 수행할 때 프로그램도 생각하고 생각해야 합니다. 하위 작업이 복잡하거나 명확하지 않은 것으로 판명되면 이에 대한 사양을 작성해야 합니다. 그러나 여기서는 코드 자체에 대해 말하는 것이 아닙니다. 모든 프로그래밍 언어, 방법론을 사용할 수 있습니다. 또한 위의 어느 것도 코드를 테스트하고 디버그할 필요가 없습니다. 추상 모델이 올바르게 작성되더라도 구현에 버그가 있을 수 있습니다.

사양 작성은 코딩 프로세스의 추가 단계입니다. 덕분에 적은 노력으로 많은 오류를 잡을 수 있습니다. Amazon 프로그래머의 경험을 통해 이를 알고 있습니다. 사양이 있으면 프로그램의 품질이 높아집니다. 그렇다면 왜 우리는 종종 그것들 없이 지내는 것일까요? 글쓰기가 어렵기 때문이다. 그리고 글쓰기는 어렵습니다. 이를 위해서는 생각이 필요하고 생각도 어렵 기 때문입니다. 당신이 생각하는 척하는 것이 항상 더 쉽습니다. 여기에서 달리기와 비유할 수 있습니다. 덜 달리면 덜 달리게 됩니다. 근육을 단련하고 글쓰기 연습을 해야 합니다. 연습이 필요합니다.

사양이 올바르지 않을 수 있습니다. 어디선가 실수를 했거나 요구 사항이 변경되었거나 개선이 필요할 수 있습니다. 누구나 사용하는 모든 코드는 변경되어야 하므로 조만간 사양이 더 이상 프로그램과 일치하지 않게 될 것입니다. 이상적으로는 이 경우 새 사양을 작성하고 코드를 완전히 다시 작성해야 합니다. 우리는 아무도 그렇게 하지 않는다는 것을 잘 알고 있습니다. 실제로는 코드를 패치하고 가능하면 사양을 업데이트합니다. 이것이 조만간 일어날 수밖에 없다면, 왜 스펙을 작성해야 할까요? 첫째, 당신의 코드를 편집할 사람에게는 사양의 모든 추가 단어가 금과 같은 가치가 있을 것이며 이 사람은 당신 자신일 수도 있습니다. 나는 종종 코드를 편집할 때 충분한 사양을 얻지 못한 것에 대해 스스로를 꾸짖습니다. 그리고 코드보다 사양을 더 많이 씁니다. 따라서 코드를 편집할 때 사양을 항상 업데이트해야 합니다. 둘째, 개정판이 있을 때마다 코드가 더 나빠지고 읽고 유지하기가 점점 더 어려워집니다. 이것은 엔트로피의 증가입니다. 그러나 사양으로 시작하지 않으면 작성하는 모든 줄이 편집되고 코드가 처음부터 다루기 힘들고 읽기 어렵습니다.

말한대로 아이젠하워, 계획에 의해 승리한 전투는 없었고, 계획 없이 승리한 전투도 없었다. 그리고 그는 전투에 대해 한두 가지를 알고 있었습니다. 스펙을 쓰는 것은 시간낭비라는 의견이 있다. 때때로 이것은 사실이며 작업이 너무 단순해서 생각할 것이 없습니다. 하지만 명세서를 쓰지 말라는 말은 생각하지 말라는 말을 듣는다는 사실을 항상 기억해야 합니다. 그리고 매번 생각해야 합니다. 작업을 생각한다고 해서 실수하지 않는다는 보장은 없습니다. 아시다시피 마술 지팡이는 아무도 발명하지 않았으며 프로그래밍은 어려운 작업입니다. 그러나 문제를 깊이 생각하지 않으면 실수할 수밖에 없습니다.

특별 웹사이트에서 TLA + 및 PlusCal에 대한 자세한 내용을 읽을 수 있습니다. 제 홈페이지에서 해당 웹사이트로 이동할 수 있습니다. 링크. 그게 전부입니다. 관심을 가져 주셔서 감사합니다.

번역본이니 참고하세요. 댓글을 작성할 때 작성자가 댓글을 읽지 않는다는 점을 기억하세요. 저자와 정말로 대화하고 싶다면 2019년 11월 12일부터 2019일까지 상트페테르부르크에서 열리는 Hydra XNUMX 컨퍼런스에 참석할 것입니다. 티켓 구매 가능 공식 웹 사이트.

출처 : habr.com