본문으로 이동

자료형 안전

위키백과, 우리 모두의 백과사전.
자료형 체계
일반 개념
주요 분류
사소한 분류

컴퓨터 과학에서 자료형 안전 또는 타입 안정성(type safety)은 프로그래밍 언어가 타입 오류를 방지하거나 막는 정도를 말한다. 타입 안전 언어는 때때로 강력하게 또는 엄격하게 타입이 지정된 언어라고도 불린다. 주어진 프로그래밍 언어에서 타입 오류로 분류되는 동작은 일반적으로 적절한 자료형이 아닌 값에 대해 연산을 수행하려는 시도로 인해 발생하는 것이다. 예를 들어, 문자열을 정수형에 더하려고 하는 경우 등이 있다.

타입 강제는 정적(잠재적 오류를 컴파일 타임에 잡아냄), 동적(런타임에 값과 타입 정보를 연결하고 필요에 따라 임박한 오류를 감지하기 위해 이를 참조함), 또는 둘의 조합일 수 있다.[1] 동적 타입 강제는 정적 강제 하에서는 유효하지 않을 프로그램을 실행할 수 있지만, 런타임에 오류를 발생시킬 수 있다는 단점이 있다.

정적(컴파일 타임) 타입 시스템의 맥락에서 타입 안전성은 일반적으로 (다른 것들과 함께) 어떤 식의 최종 값이 그 식의 정적 타입의 합법적인 멤버가 될 것이라는 보장을 포함한다. 정확한 요구사항은 이보다 더 미묘한데, 예를 들어 서브타이핑과 다형성과 같은 복잡성을 참조하라.

정의

[편집]

직관적으로 타입 건전성은 로빈 밀너의 간결한 진술에 포착되어 있다.

타입이 잘 지정된 프로그램은 "잘못되지" 않는다.[2]

다시 말해, 타입 시스템이 건전하다면, 그 타입 시스템에 의해 허용된 식은 적절한 타입의 값으로 평가되어야 한다(다른 무관한 타입의 값을 생성하거나 타입 오류로 인해 충돌하는 대신). 비자이 사라사와트는 다음과 같은 관련 정의를 제공한다.

언어는 데이터에 대해 수행할 수 있는 유일한 연산이 데이터 타입에 의해 승인된 것일 경우 타입 안전하다.[3]

그러나 프로그램이 "타입이 잘 지정되었다"거나 "잘못된다"는 것이 정확히 무엇을 의미하는지는 해당 프로그래밍 언어에 특정한 정적 및 동적 의미론의 속성이다. 따라서 타입 건전성에 대한 정확하고 형식적인 정의는 언어를 지정하는 데 사용되는 형식 의미론의 스타일에 따라 달라진다. 1994년에 앤드류 라이트와 마티아스 펠라이젠은 동작적 의미론에 의해 정의된 언어에서 타입 안전성에 대한 표준 정의 및 증명 기법을 공식화했다.[4] 이는 대부분의 프로그래머가 이해하는 타입 안전성 개념에 가장 가깝다. 이 접근 방식에 따라 언어의 의미론은 타입 건전하다고 간주되기 위해 다음 두 가지 속성을 가져야 한다.

진행
타입이 잘 지정된 프로그램은 결코 "멈추지" 않는다. 모든 식은 이미 값이거나 어떤 잘 정의된 방식으로 값으로 축소될 수 있다. 다시 말해, 프로그램은 더 이상 전환이 불가능한 미정의 상태에 빠지지 않는다.
보존 (또는 서브젝트 리덕션)
각 평가 단계 후에 각 식의 타입은 동일하게 유지된다(즉, 타입이 보존된다).

타입 건전성에 대한 여러 다른 형식적 처리 방법도 표시적 의미론 및 구조적 동작 의미론의 관점에서 발표되었다.[2][5][6]

다른 형태의 안전성과의 관계

[편집]

고립된 상태에서 타입 건전성은 비교적 약한 속성이다. 본질적으로 타입 시스템의 규칙이 내부적으로 일관되며 전복될 수 없음을 나타낼 뿐이기 때문이다. 그러나 실제로는 프로그래밍 언어가 잘 타입화되면 다른 더 강력한 속성도 수반하도록 설계되며, 그 중 일부는 다음과 같다.

  • 불법적인 연산 방지. 예를 들어, 타입 시스템은 3 / "Hello, World"라는 식을 유효하지 않은 것으로 거부할 수 있다. 나누기 연산자가 문자열 약수에 대해 정의되지 않았기 때문이다.
  • 메모리 보안
    • 타입 시스템은 특정 타입의 객체에 대한 포인터가 다른 타입의 객체에 대한 포인터로 처리될 때 발생할 수 있는 허상 포인터를 방지할 수 있다.
    • 의존형을 지원하는 것과 같은 더 정교한 타입 시스템은 범위를 벗어난 접근을 감지하고 거부하여 잠재적인 버퍼 오버플로를 방지할 수 있다.[7]
  • 다른 타입의 의미론에서 발생하는 논리 오류. 예를 들어, 인치와 밀리미터는 모두 정수로 저장될 수 있지만 서로 대체되거나 더해져서는 안 된다. 타입 시스템은 이들에 대해 두 가지 다른 정수 타입을 강제할 수 있다.

타입 안전 언어와 타입 불안전 언어

[편집]

타입 안전성은 일반적으로 학술 프로그래밍 언어 연구에서 제안되는 모든 장난감 언어(즉, 난해한 프로그래밍 언어)의 요구 사항이다. 반면에 많은 언어는 인간이 생성하는 타입 안전성 증명에는 너무 커서 수천 가지 경우를 확인해야 하는 경우가 많다. 그럼에도 불구하고, 엄격하게 정의된 의미론을 가진 표준 ML과 같은 일부 언어는 타입 안전성의 한 가지 정의를 충족하는 것으로 입증되었다.[8] 하스켈과 같은 일부 다른 언어는 특정 "탈출" 기능이 사용되지 않는 한 타입 안전성의 어떤 정의를 충족한다고 여겨진다틀:Discuss(예를 들어, I/O가 가능한 일반적인 제한된 환경에서 "탈출"하는 데 사용되는 하스켈의 unsafePerformIO는 타입 시스템을 우회하여 타입 안전성을 깨뜨릴 수 있다.[9]) 타입 펀닝은 이러한 "탈출" 기능의 또 다른 예이다. 언어 정의의 속성과 관계없이 구현의 버그나 다른 언어로 작성된 연결된 라이브러리로 인해 런타임에 특정 오류가 발생할 수 있다. 이러한 오류는 특정 상황에서 주어진 구현을 타입 불안전하게 만들 수 있다. 초기 버전의 선 마이크로시스템즈 자바 가상 머신은 이러한 종류의 문제에 취약했다.[3]

강력한 타입과 약한 타입

[편집]

프로그래밍 언어는 종종 타입 안전성의 특정 측면을 지칭하기 위해 강력하게 타입이 지정되었거나 약하게 타입이 지정되었다(느슨하게 타입이 지정되었다고도 함)고 통속적으로 분류된다. 1974년에 리스코프와 질레스는 강력하게 타입이 지정된 언어를 "객체가 호출 함수에서 호출된 함수로 전달될 때마다 그 타입이 호출된 함수에 선언된 타입과 호환되어야 하는" 언어라고 정의했다.[10] 1977년에 잭슨은 "강력하게 타입이 지정된 언어에서는 각 데이터 영역이 고유한 타입을 가지며 각 프로세스는 이러한 타입의 관점에서 통신 요구 사항을 명시할 것이다"라고 썼다.[11] 대조적으로, 약하게 타입이 지정된 언어는 예측할 수 없는 결과를 생성하거나 암시적 타입 변환을 수행할 수 있다.[12]

메모리 관리 및 자료형 안전

[편집]

자료형 안전은 메모리 보안과 밀접하게 연관되어 있다. 예를 들어, 특정 비트 패턴은 허용하지만 다른 비트 패턴은 허용하지 않는 타입 를 가진 언어의 구현에서, 허상 포인터 메모리 오류는 타입의 죽은 변수에 의 유효한 멤버를 나타내지 않는 비트 패턴을 쓰는 것을 허용하여, 변수를 읽을 때 타입 오류를 유발한다. 반대로, 언어가 메모리 안전하다면, 임의의 정수를 포인터로 사용하는 것을 허용할 수 없으므로, 별도의 포인터 또는 참조 타입이 있어야 한다.

최소한의 조건으로, 타입 안전 언어는 다른 타입의 할당에 걸쳐 허상 포인터를 허용해서는 안 된다. 그러나 대부분의 언어는 메모리 안전성이나 어떤 종류의 치명적인 오류 방지를 위해 엄격하게 필요하지 않더라도 프로그래머가 정의한 추상 자료형의 적절한 사용을 강제한다. 할당은 그 내용물을 설명하는 타입을 부여받으며, 이 타입은 할당 기간 동안 고정된다. 이를 통해 타입 기반의 별칭 분석이 다른 타입의 할당이 구별된다고 추론할 수 있다.

대부분의 타입 안전 언어는 쓰레기 수집을 사용한다. 피어스(Pierce)는 허상 포인터 문제 때문에 "명시적인 할당 해제 연산이 있는 상황에서 타입 안전성을 달성하는 것은 극히 어렵다"고 말한다.[13] 그러나 러스트는 일반적으로 타입 안전하다고 여겨지며, 쓰레기 수집 대신 빌림 검사기(borrow checker)를 사용하여 메모리 안전성을 달성한다.

객체 지향 언어의 타입 안전성

[편집]

객체 지향 언어에서 타입 안전성은 일반적으로 자료형 체계가 존재한다는 사실에 내재되어 있다. 이는 클래스 정의 측면에서 표현된다.

클래스는 본질적으로 그로부터 파생된 객체들의 구조와 이 객체들을 처리하기 위한 계약으로서의 API를 정의한다. 새로운 객체가 생성될 때마다 그 계약을 준수하게 된다.

특정 클래스에서 파생되거나 특정 인터페이스를 구현하는 객체를 교환하는 각 함수는 해당 계약을 준수할 것이다. 따라서 해당 함수에서 해당 객체에 허용되는 연산은 객체가 구현하는 클래스의 메서드에 의해 정의된 것들뿐이다. 이는 객체의 무결성이 보존되도록 보장할 것이다.[14]

이것에 대한 예외는 객체 구조의 동적 수정을 허용하는 객체 지향 언어나, 클래스 메서드 정의에 의해 부과된 제약을 극복하기 위해 리플렉션을 사용하여 객체의 내용을 수정하는 경우이다.

특정 언어의 타입 안전성 문제

[편집]

에이다

[편집]

에이다는 임베디드 시스템, 장치 드라이버 및 기타 형태의 시스템 프로그래밍에 적합하도록 설계되었지만, 타입 안전 프로그래밍을 장려하도록 설계되기도 했다. 이러한 상충되는 목표를 해결하기 위해 에이다는 타입 불안전성을 보통 Unchecked_ 문자열로 시작하는 이름의 특정 특수 구성 집합으로 제한한다. Unchecked_Deallocation은 이 유닛에 pragma Pure를 적용함으로써 에이다 텍스트 유닛에서 효과적으로 금지될 수 있다. 프로그래머는 Unchecked_ 구성을 매우 신중하게, 그리고 필요한 경우에만 사용할 것으로 예상된다. 이를 사용하지 않는 프로그램은 타입 안전하다.

SPARK 프로그래밍 언어는 에이다의 모든 잠재적 모호성과 불안정성을 제거하면서 동시에 언어 기능에 정적으로 검사되는 계약을 추가한 에이다의 부분 집합이다. SPARK는 런타임에 할당을 완전히 허용하지 않음으로써 허상 포인터 문제를 피한다.

에이다 2012는 언어 자체에 정적으로 검사되는 계약을 추가한다 (사전 및 사후 조건, 그리고 타입 불변식의 형태로).

C

[편집]

C 프로그래밍 언어는 제한된 맥락에서 타입 안전하다. 예를 들어, 명시적 캐스트가 사용되지 않는 한 한 타입의 구조체에 대한 포인터를 다른 타입의 구조체에 대한 포인터로 변환하려는 시도는 컴파일 타임 오류를 발생시킨다. 그러나 많은 일반적인 연산은 타입 안전하지 않다. 예를 들어, 정수를 출력하는 일반적인 방법은 printf("%d", 12)와 같은데, 여기서 %d는 printf에게 런타임에 정수 인수를 예상하도록 지시한다. (printf("%s", 12)와 같은, 함수에게 문자열에 대한 포인터를 예상하도록 지시하면서 정수 인수를 제공하는 것은 컴파일러에 의해 허용될 수 있지만, 정의되지 않은 결과를 생성할 것이다.) 이는 일부 컴파일러(예: gcc)가 printf 인수와 형식 문자열 간의 타입 일치 여부를 확인함으로써 부분적으로 완화된다.

또한, C는 에이다와 마찬가지로 명시적이고 불분명하거나 정의되지 않은 변환을 제공한다. 그리고 에이다와는 달리, 이러한 변환을 사용하는 관용구는 매우 흔하며, C에 타입 불안전하다는 평판을 안겨주는 데 일조했다. 예를 들어, 힙에 메모리를 할당하는 표준적인 방법은 필요한 바이트 수를 나타내는 인자와 함께 malloc과 같은 메모리 할당 함수를 호출하는 것이다. 이 함수는 void 포인터 (void*)를 반환하며, 호출 코드는 이를 명시적으로 또는 암시적으로 적절한 포인터 타입으로 캐스트해야 한다. C의 표준화 이전 구현에서는 이를 위해 명시적 캐스트가 필요했으므로, struct Foo의 할당을 위해 Foo* foo = (struct Foo*)malloc(sizeof(struct Foo)) 코드가 일반적인 관행이 되었다.[15] malloc()은 void*를 반환하며 C에서는 명시적으로 캐스트할 필요가 없지만, C++에서는 타입 안전성을 위해 이 캐스팅이 의무화된다.

C++

[편집]

보다 타입 안전한 코드를 촉진하는 C++의 일부 기능:

C#

[편집]

C 샤프는 타입 안전하다. 타입이 지정되지 않은 포인터를 지원하지만, 이는 컴파일러 수준에서 금지될 수 있는 "unsafe" 키워드를 사용하여 접근해야 한다. 런타임 캐스트 유효성 검사를 위한 내재적 지원을 제공한다. 캐스트는 유효하지 않은 경우 null 참조를 반환하는 "as" 키워드를 사용하거나, 유효하지 않은 경우 예외를 발생시키는 C 스타일 캐스트를 사용하여 유효성을 검사할 수 있다. C 샤프 변환 연산자를 참조하라.

모든 다른 타입이 파생되는 객체 타입에 과도하게 의존하는 것은 C# 타입 시스템의 목적을 무력화시킬 위험이 있다. 일반적으로 .NET의 제네릭 프로그래밍|제네릭을 선호하여 객체 참조를 포기하는 것이 더 나은 관행이다.

자바

[편집]

자바 언어는 타입 안전성을 강제하도록 설계되었다. 자바의 모든 것은 객체 내에서 발생하며 각 객체는 클래스의 인스턴스이다.

타입 안전성 강제를 구현하기 위해 각 객체는 사용 전에 할당되어야 한다. 자바는 원시 자료형의 사용을 허용하지만, 이는 적절하게 할당된 객체 내에서만 가능하다.

때때로 타입 안전성의 일부는 간접적으로 구현된다. 예를 들어, `BigDecimal` 클래스는 임의 정밀도의 부동 소수점 숫자를 나타내지만, 유한한 표현으로 나타낼 수 있는 숫자만 처리한다. `BigDecimal.divide()` 연산은 `BigDecimal`로 표현된 두 숫자의 나눗셈으로 새 객체를 계산한다.

이 경우 나눗셈에 유한한 표현이 없는 경우 (예: 1/3=0.33333... 계산 시), 연산에 대해 반올림 모드가 정의되지 않으면 `divide()` 메서드가 예외를 발생시킬 수 있다. 따라서 언어보다는 라이브러리가 클래스 정의에 내재된 계약을 객체가 준수하도록 보장한다.

표준 ML

[편집]

표준 ML은 엄격하게 정의된 의미론을 가지며 타입 안전하다는 것이 알려져 있다. 그러나 Standard ML of New Jersey (SML/NJ), 그 구문 변형인 Mythryl, 그리고 MLton을 포함한 일부 구현은 안전하지 않은 연산을 제공하는 라이브러리를 제공한다. 이러한 기능은 종종 특정 방식으로 데이터가 배치되어야 할 수 있는 비-ML 코드(예: C 라이브러리)와 상호 작용하기 위해 해당 구현의 외부 함수 인터페이스와 함께 사용된다. 또 다른 예는 SML/NJ 대화형 최상위 수준 자체로, 사용자가 입력한 ML 코드를 실행하기 위해 안전하지 않은 연산을 사용해야 한다.

모듈라-2

[편집]

모듈라-2는 강력하게 타입이 지정된 언어로, 안전하지 않은 기능을 명시적으로 안전하지 않은 것으로 표시하도록 요구하는 설계 철학을 가지고 있다. 이는 그러한 기능을 SYSTEM이라는 내장된 유사 라이브러리로 "이동"시켜 사용하기 전에 가져와야 함으로써 달성된다. 따라서 가져오기는 그러한 기능이 사용될 때 가시적으로 만든다. 불행히도, 이는 원래 언어 보고서와 그 구현에서 일관되게 구현되지 않았다.[16] 타입 캐스트 구문과 (파스칼에서 상속된) 변형 레코드와 같이 사전 가져오기 없이 사용할 수 있는 안전하지 않은 기능이 여전히 남아 있었다.[17] 이러한 기능을 SYSTEM 유사 모듈로 이동하는 어려움은 가져올 수 있는 식별자가 없다는 것이었다. 식별자만 가져올 수 있고 구문은 가져올 수 없었기 때문이다. 

IMPORT SYSTEM; (* allows the use of certain unsafe facilities: *)
VAR word : SYSTEM.WORD; addr : SYSTEM.ADDRESS;
addr := SYSTEM.ADR(word);

(* but type cast syntax can be used without such import *)
VAR i : INTEGER; n : CARDINAL;
n := CARDINAL(i); (* or *) i := INTEGER(n);

ISO 모듈라-2 표준은 타입 캐스트 구문을 유사 모듈 SYSTEM에서 가져와야 하는 CAST라는 함수로 변경하여 타입 캐스트 기능을 수정했다. 그러나 변형 레코드와 같은 다른 안전하지 않은 기능은 유사 모듈 SYSTEM에서 가져오지 않아도 계속 사용할 수 있었다.[18] 

IMPORT SYSTEM;
VAR i : INTEGER; n : CARDINAL;
i := SYSTEM.CAST(INTEGER, n); (* Type cast in ISO Modula-2 *)

언어의 최근 개정판은 원래의 설계 철학을 엄격하게 적용했다. 먼저, 유사 모듈 SYSTEM은 UNSAFE로 이름이 변경되어 그곳에서 가져온 기능의 안전하지 않은 특성을 더욱 명확하게 했다. 그런 다음 나머지 안전하지 않은 기능은 완전히 제거되거나(예: 변형 레코드) UNSAFE 유사 모듈로 이동되었다. 가져올 수 있는 식별자가 없는 기능의 경우, 활성화 식별자가 도입되었다. 그러한 기능을 활성화하려면 해당 활성화 식별자를 UNSAFE 유사 모듈에서 가져와야 한다. UNSAFE에서 가져오기를 요구하지 않는 안전하지 않은 기능은 언어에 남아있지 않다.[17] 

IMPORT UNSAFE;
VAR i : INTEGER; n : CARDINAL;
i := UNSAFE.CAST(INTEGER, n); (* Type cast in Modula-2 Revision 2010 *)

FROM UNSAFE IMPORT FFI; (* enabling identifier for foreign function interface facility *)
<*FFI="C"*> (* pragma for foreign function interface to C *)

파스칼

[편집]

파스칼은 여러 가지 타입 안전성 요구 사항을 가지고 있었으며, 그중 일부는 일부 컴파일러에서 유지되고 있다. 파스칼 컴파일러가 "엄격한 타이핑"을 지시하는 경우, 두 변수는 호환되는 경우(예: 정수에서 실수로의 변환) 또는 동일한 서브타입에 할당된 경우가 아니면 서로 할당될 수 없다. 예를 들어, 다음과 같은 코드 조각이 있다고 가정해 보자. 

type
  TwoTypes = record
     I: Integer;
     Q: Real;
  end;

  DualTypes = record
    I: Integer;
    Q: Real;
  end;

var
  T1, T2:  TwoTypes;
  D1, D2:  DualTypes;

엄격한 타이핑 하에서는 TwoTypes로 정의된 변수는 DualTypes와 호환되지 않는다(동일하지 않기 때문에, 비록 사용자 정의 타입의 구성 요소가 동일하더라도). 따라서 T1 := D2; 할당은 불법이다. T1 := T2; 할당은 정의된 서브타입이 동일하므로 합법적이다. 그러나 T1.Q := D1.Q;와 같은 할당은 합법적이다.

커먼 리스프

[편집]

일반적으로 커먼 리스프는 타입 안전 언어이다. 커먼 리스프 컴파일러는 타입 안전성을 정적으로 증명할 수 없는 연산에 대해 동적 검사를 삽입할 책임이 있다. 그러나 프로그래머는 프로그램이 더 낮은 수준의 동적 타입 검사로 컴파일되어야 함을 나타낼 수 있다.[19] 이러한 모드로 컴파일된 프로그램은 타입 안전하다고 간주할 수 없다.

C++ 예제

[편집]

다음 예제는 C++ 캐스트 연산자가 잘못 사용될 때 어떻게 타입 안전성을 깨뜨릴 수 있는지 보여준다. 첫 번째 예제는 기본 자료형이 어떻게 잘못 캐스팅될 수 있는지 보여준다. 

#include <iostream>
using namespace std;

int main () {
    int   ival = 5;                              // integer value
    float fval = reinterpret_cast<float&>(ival); // reinterpret bit pattern
    cout << fval << endl;                        // output integer as float
    return 0;
}

이 예제에서 reinterpret_cast는 컴파일러가 정수에서 부동 소수점 값으로 안전한 변환을 수행하는 것을 명시적으로 방지한다.[20] 프로그램이 실행될 때 쓰레기 부동 소수점 값이 출력될 것이다. float fval = ival;이라고 대신 작성했다면 이 문제는 피할 수 있었을 것이다.

다음 예제는 객체 참조가 어떻게 잘못 다운캐스트될 수 있는지 보여준다. 

#include <iostream>
using namespace std;

class Parent {
public:
    virtual ~Parent() {} // virtual destructor for RTTI
};

class Child1 : public Parent {
public:
    int a;
};

class Child2 : public Parent {
public:
    float b;
};

int main () {
    Child1 c1;
    c1.a = 5;
    Parent & p = c1;                     // upcast always safe
    Child2 & c2 = static_cast<Child2&>(p); // invalid downcast
    cout << c2.b << endl;          // will output garbage data
    return 0;
}

두 자식 클래스는 서로 다른 타입의 멤버를 가지고 있다. 부모 클래스 포인터를 자식 클래스 포인터로 다운캐스트할 때, 결과 포인터가 올바른 타입의 유효한 객체를 가리키지 않을 수 있다. 이 예제에서는 쓰레기 값이 출력되는 결과를 초래한다. static_cast를 유효하지 않은 캐스트에 예외를 던지는 dynamic_cast로 대체했다면 이 문제를 피할 수 있었을 것이다.[21]

같이 보기

[편집]

내용주

[편집]
  1. ↑ “What to know before debating type systems | Ovid [blogs.perl.org]”. 《blogs.perl.org》. 2023년 6월 27일에 확인함. 
  2. ↑ 가 나 Milner, Robin (1978), “A Theory of Type Polymorphism in Programming”, 《Journal of Computer and System Sciences》 17 (3): 348–375, doi:10.1016/0022-0000(78)90014-4, hdl:20.500.11820/d16745d7-f113-44f0-a7a3-687c2b709f66 
  3. ↑ 가 나 Saraswat, Vijay (1997년 8월 15일). “Java is not type-safe”. 2008년 10월 8일에 확인함. 
  4. ↑ Wright, A. K.; Felleisen, M. (1994년 11월 15일). 《A Syntactic Approach to Type Soundness》 (영어). 《Information and Computation》 115. 38–94쪽. doi:10.1006/inco.1994.1093. ISSN 0890-5401. 
  5. ↑ Damas, Luis; Milner, Robin (1982년 1월 25일). 〈Principal type-schemes for functional programs〉. 《Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '82》. Association for Computing Machinery. 207–212쪽. doi:10.1145/582153.582176. ISBN 0897910656. S2CID 11319320. 
  6. ↑ Tofte, Mads (1988). 《Operational Semantics and Polymorphic Type Inference》 (영어) (학위논문). 
  7. ↑ Henriksen, Troels; Elsman, Martin (2021년 6월 17일). 〈Towards size-dependent types for array programming〉. 《Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming》. Association for Computing Machinery. 1–14쪽. doi:10.1145/3460944.3464310. ISBN 9781450384667. S2CID 235474098. 
  8. ↑ Standard ML. Smlnj.org. Retrieved on 2013-11-02.
  9. ↑ “System.IO.Unsafe”. 《GHC libraries manual: base-3.0.1.0》. 2008년 7월 5일에 원본 문서에서 보존된 문서. 2008년 7월 17일에 확인함. 
  10. ↑ Liskov, B; Zilles, S (1974). 《Programming with abstract data types》. 《ACM SIGPLAN Notices》 9. 50–59쪽. CiteSeerX 10.1.1.136.3043. doi:10.1145/942572.807045. 
  11. ↑ Jackson, K. (1977). 〈Parallel processing and modular software construction〉. 《Design and Implementation of Programming Languages》. Lecture Notes in Computer Science 54. 436–443쪽. doi:10.1007/BFb0021435. ISBN 3-540-08360-X. 
  12. ↑ “CS1130. Transition to OO programming. – Spring 2012 --self-paced version”. Cornell University, Department of Computer Science. 2005. 2023년 9월 15일에 확인함. 
  13. ↑ Pierce, Benjamin C. (2002). 《Types and programming languages》. Cambridge, Mass.: MIT Press. 158쪽. ISBN 0-262-16209-1. 
  14. ↑ 타입 안전성은 따라서 좋은 클래스 정의의 문제이기도 하다: 객체의 내부 상태를 수정하는 public 메서드는 객체의 무결성을 보존해야 한다.
  15. ↑ Kernighan; Dennis M. Ritchie (March 1988). 《The C Programming Language》 2판. Englewood Cliffs, NJ: Prentice Hall. 116쪽. ISBN 978-0-13-110362-7. In C, the proper method is to declare that malloc returns a pointer to void, then explicitly coerce the pointer into the desired type with a cast. 
  16. ↑ Niklaus Wirth (1985). 《Programming in Modula-2》. Springer Verlag. 
  17. ↑ 가 나 “The Separation of Safe and Unsafe Facilities”. 2015년 3월 24일에 확인함. 
  18. ↑ “ISO Modula-2 Language Reference”. 2015년 3월 24일에 확인함. 
  19. ↑ “Common Lisp HyperSpec”. 2013년 5월 26일에 확인함. 
  20. ↑ “reinterpret_cast conversion - cppreference.com”. En.cppreference.com. 2022년 9월 21일에 확인함. 
  21. ↑ “dynamic_cast conversion - cppreference.com”. En.cppreference.com. 2022년 9월 21일에 확인함. 

각주

[편집]
원본 주소 "https://ko.wikipedia.org/w/index.php?title=자료형_안전&oldid=40834709"