이 문서는 ‘Introduction To SPARK'(저자: Claire Dross, Yannick Moy, © AdaCore 2018–2024)를 Google Gemini가 한국어로 번역한 것입니다. 원저작물과 동일하게 CC BY 4.0 라이선스가 적용됩니다.
이 튜토리얼은 SPARK 프로그래밍 언어와 그 정형 검증(formal verification) 도구에 대한 인터랙티브(상호작용형) 입문 과정입니다. 여러분은 에이다(Ada)와 SPARK의 차이점을 배우고, SPARK와 함께 제공되는 다양한 분석 도구를 사용하는 방법을 익히게 될 것입니다.
이 문서는 Claire Dross와 Yannick Moy가 작성했습니다.
참고
이 과정의 코드 예제는 80 컬럼(열) 제한을 사용하는데, 이는 에이다(Ada) 코드의 일반적인 제한입니다. 작은 화면 크기의 장치에서는 일부 코드 예제가 읽기 어려울 수 있습니다.
목차:
현재 번역 중입니다.