불변은 무엇입니까?

불변은 무엇입니까?

---

이 단어는 여러 상황에서 사용되는 것입니다. 내가 알 수있는 가장 좋은 의미가 변할 수없는 변수를 의미한다는 것입니다. 그 상수 / 최종 (자바 Java!)이 아닌가?

---

불변은 변수보다 "개념적"입니다. 일반적으로 항상 참인 프로그램 상태의 속성입니다. 불변 값 보유를 보장하는 함수 또는 방법은 불변 값을 유지합니다.

예를 들어, 이진 검색 트리에는 모든 노드에 대해 노드의 왼쪽 노드 키가 노드의 자체 키보다 작은 것이 변하지 않을 수 있습니다. 이 트리에 존재하는 내부 함수는 해당 불변성을 유지합니다.

아시다시피, 그것은 변수에 수있는 종류의 것이 아닙니다 . 프로그램 에 대한 설명 입니다. 프로그램이 유지해야 할 불변의 종류를 수행 한 다음 코드를 검토하여 불변을 유지하는지 확인하는 코드의 위치 오류를 피할 수 있습니다.

---

그것은 당신이 당신의 논리의 특정 장소에서 항상 참이라는 것을 알고 조건이 무엇 이냐 해결하기 위해 위해 할 때 확인할 수 있습니다.

---

나는 보통 알고리즘이나 구조에서 더 많이 본다.

예를 들어, 각 반복의 시작 또는 끝에서 항상 주장 할 수있는 루프 불변 값을 수 있습니다. 즉, 루프가 한 스택에서 다른 스택으로 수집을 처리해야한다면 루프의 맨 위 또는 맨 아래에 | stack1 | + | stack2 | = c라고 말할 수 있습니다.

불변 검사가 실패하면 문제가 있음을 나타냅니다. 이 예에서는 처리 된 요소를 최종 스택 등으로 푸시하는 것을 잊었을 의미 할 수 있습니다.

---

위키 백과의 마술 : 불변 (컴퓨터 과학)

컴퓨터 과학에서, 만약 그것이 사실이라면, 동작 시퀀스 내내 진실을 유지하고 술어는 그 시퀀스에 불변이라고 불린다.

---

이 줄은 다음과 같이 사실.

컴퓨터 과학에서, 만약 그것이 사실이라면, 동작 시퀀스 내내 진실을 유지하고 술어는 그 시퀀스에 불변이라고 불린다.

이 희망을 더 잘 이해하기 위해 C ++ 의이 예제가 도움이됩니다.

일부 값을 가져 오기로 가져 오는 변수에서 그 수를 가져 오기로 변수라는 변수에 count추가 해야하는 시나리오를 고려하십시오.sum

불변는 (다시 더 많은 개념처럼) :

// invariant:
// we have read count grades so far, and
// sum is the sum of the first count grades

위의 코드는 다음과 가변됩니다.

int count=0;
double sum=0,x=0;
while (cin >> x) {
++count;
sum+=x;
}

위의 코드는 무엇입니까?

1) 입력을 읽고 입력 cin합니다x

2) 번 읽은 후에 한 증가는 count시키고sum = sum + x

3) 1 ~ 2를 반복하십시오.

불변 루프 :

불변 값은 항상 참이어야합니다 . 처음에는이 코드로 코드를 시작합니다

while(cin>>x){
  }

이 루프는 표준 입력에서 데이터를 읽고 x에 저장합니다. 잘하고 좋아. 그러나 우리의 불변 의 첫-th 부분이 따르지 않았기 때문에 (또는 사실로 유지됨) 불변 은 거짓이됩니다 .

// we have read count grades so far, and

변하지 않는 사실을 유지하는 방법?

단순한! 증분 발행.

그래서 ++count;잘 할 것입니다! 이제 코드는 다음과 같이됩니다.

while(cin>>x){
 ++count; 
 }

그러나

지금도 우리의 불변 지금 우리의 두 번째 부분 만족하지 사고 기 때문에 (TRUE 궐석 개념) False입니다 우리의 불변을.

// sum is the sum of the first count grades

이제 어떻게해야해야합니까?

추가 x로 sum와에 저장 sum( sum+=x)와 다음 번에 cin>>xX에 새로운 값을 읽습니다.

이제 코드는 다음과 같이됩니다.

while(cin>>x){
 ++count; 
 sum+=x;
 }

점검 해보자

코드가 불변 값과 일치하는지 여부

// invariant:
// we have read count grades so far, and
// sum is the sum of the first count grades

암호 :

while(cin>>x){
 ++count; 
 sum+=x;
 }

아!. 이제 루프 불변은 항상 True 이며 코드는 작동합니다.

위의 예제는 Andrew-koening과 Barbara-E의 Accelerated C ++ 책 에서 가져와 수정되었습니다 .

---

코드 블록 내에서 변하지 않는 것

---

그것이 무엇에 따라 불변는 불변이 존재해야하는지 개념적으로 알고 있기 때문에, 깨끗한 코드를 작성하기에 매우 유용 에 코드가 쉽게 그 목표에 도달하기 위해 코드를 구성하는 방법을 결정할 수 있습니다. 앞서 언급했듯이, 불변이 유지되고 있는지 확인하는 것은 수행하려는 조작이 실제로 원하는 작업을 수행하는지 확인하는 좋은 방법이기 때문에 디버깅에도 유용합니다.

---

일반적으로 특정 수학적 연산에서 변경되지 않는 수량입니다. 예를 들어 회전시 변경되지 않는 스칼라가 있습니다. 예를 들어 자기 공명 영상에서는 회전 불변으로 조직 속성을 특성화하는 것이 유용합니다. 왜냐하면 그 추정은 이상적으로 스캐너에서 신체의 방향에 의존하지 않기 때문입니다.

---

ADT 불변은 인스턴스 메서드 실행 전후에 항상 참이어야하는 데이터 필드 (인스턴스 변수) 간의 관계를 지정합니다.

---

불변의 훌륭한 예가 있으며 이것이 Java Concurrency in Practice 책에 중요한 이유가 있습니다 .

Java 중심이지만 예제에서는 제공된 정수의 요소를 계산하는 일부 코드를 설명합니다. 예제 코드는 제공된 마지막 숫자와 성능 향상을 위해 계산 된 요소를 캐시하려고합니다. 이 시나리오에서는 동시 시나리오에서 경쟁 조건에 취약한 코드를 남겨둔 예제 코드에서 설명되지 않은 불변성이 있습니다.

---

여기에있는 모든 대답은 훌륭하지만 문제에 대해 더 많은 것을 밝힐 수 있다고 느꼈습니다.

언어 관점에서 불변이란 결코 변하지 않는 것을 의미합니다. 개념은 실제로 수학에서 나왔지만 귀납법과 결합 할 때 인기있는 증명 기술 중 하나입니다.

다음은 증명이 진행되는 방법입니다. 초기 상태에있는 불변을 찾을 수 있고이 불변이 상태에 적용된 [법적] 변환과 관계없이 지속된다는 것을 증명할 수 있습니다. 불변하면 초기 상태에 어떤 변환 시퀀스가 ​​적용 되더라도 결코 발생할 수 없습니다.

이제 이전의 사고 방식 (다시 귀납법과 결합)은 컴퓨터 소프트웨어의 논리를 예측할 수있게합니다. 특정 루프가 특정 결과를 산출하거나 특정 방식으로 프로그램의 상태를 변경하지 않는다는 것을 증명하기 위해 불변성을 사용할 수있는 루프에서 실행이 진행될 때 특히 중요합니다.

불변이 루프 논리를 술어하는 데 사용되는 경우 호출 된 루프 불변 입니다. 루프 외부에서 사용할 수 있지만 for 루프는 종종 많은 가능성 또는 무한한 가능성이 있기 때문에 정말 중요합니다.

내가 컴퓨터 소프트웨어의 논리를 "술어"라는 단어를 사용하고 증명하는 것이 아니라는 점에 유의하십시오. 그리고 그것은 수학에서 불변성 이 증명으로 사용될 수 있지만, 소프트웨어가 많은 추상화 위에서 실행된다는 사실 때문에 결코 증명할 수없는 컴퓨터 소프트웨어가 실행될 때 예상되는 것을 산출 할 것이라는 것을 결코 증명할 수 없기 때문입니다. 예상되는 것을 산출 할 것입니다 (예를 들어 하드웨어 추상화를 생각해보십시오).

마지막으로 소프트웨어 로직을 이론적으로 엄격하게 예측하는 것은 의료 및 군사용 애플리케이션과 같은 매우 중요한 애플리케이션에만 중요합니다. Invariant는 디버깅 할 때 일반적인 프로그래머를 돕기 위해 계속 사용할 수 있습니다. 특정 위치의 위치를 ​​아는 데 사용할 수 있습니다. 프로그램은 특정 불변성을 유지하지 못하여 실패했습니다. 우리 중 많은 사람들이 어쨌든 그것에 대해 생각하지 않고 그것을 사용합니다.

참고 URL : https://stackoverflow.com/questions/112064/what-is-an-invariant