Ada 프로그래밍: 10. SPARK 소개

나르시

2025.08.11 00:27:30

조회 114 추천 0 댓글 0

10. SPARK 소개

SPARK(SPADE Ada Kernel의 합성어)는 고신뢰성 소프트웨어 개발을 위해 특별히 설계된 Ada 언어의 형식적으로 분석 가능한 하위 집합입니다.

SPARK는 두 가지 전략의 조합을 통해 정확성 증명을 가능하게 하는 목표를 달성합니다:

언어 부분집합화: 일반적인 접근 형식(에일리어싱 방지), 예외 처리(모든 런타임 오류가 없음을 증명하므로), 함수 내 부작용 등 형식적으로 분석하기 어려운 Ada의 기능을 제외합니다.
강화된 계약: Ada의 DbC 모델을 확장하여 데이터 의존성(어떤 입력이 어떤 출력에 영향을 미치는지), 정보 흐름 정책, 상태 추상화와 같은 속성을 지정할 수 있는 더 상세한 계약을 추가합니다.

GNATprove와 같은 도구 모음을 사용하여 개발자는 형식적 방법을 통해 수학적 증명의 높은 확신도로 SPARK 프로그램이 언어 정의 런타임 오류로부터 자유롭고, 기능적 명세를 준수하며, 중요한 안전 및 보안 속성을 준수함을 증명할 수 있습니다. 이는 테스트(버그의 존재만을 보여줄 수 있음)를 넘어 증명(버그의 부재를 보여줄 수 있음)으로 나아가는 높은 수준의 소프트웨어 보증을 나타냅니다. 강력한 형식 시스템에서부터 런타임 검사, 계약에 의한 설계, 그리고 SPARK를 이용한 형식적 증명에 이르기까지 이 계층적 접근 방식이 Ada 언어 제품군을 고무결성 소프트웨어 구축에 적합하게 만듭니다.

고정닉 0

전체 댓글 0개

등록순 최신순 답글순

본문 보기

타인의 권리를 침해하거나 명예를 훼손하는 댓글은 운영원칙 및 관련 법률에 제재를 받을 수 있습니다.
Shift+Enter 키를 동시에 누르면 줄바꿈이 됩니다.

갤러리 리스트
번호	제목	글쓴이	작성일	조회	추천
설문	영포티룩도 멋지게 소화할 것 같은 40대 스타는?	운영자	25/10/27	-	-
AD	할로윈 슈퍼위크~!!	운영자	25/10/23	-	-
공지	프로그래밍 갤러리 이용 안내 [97]	운영자	20.09.28	48271	65
2899010	나는 코딩에 재능은 없지만 코딩은 좋아함	ㅆㅇㅆ(124.216)	23:02	6	0
2899005	명상 하다보니 러스트 프로그래밍보다 인생이란 뭘까 [3]	프갤러(110.8)	22:45	16	0
2899004	나는 모든인간들이 나처럼 인생살았으면 좋겠음 [1]	타이밍뒷.통수한방(1.213)	22:38	19	0
2899003	명상 하다가 현타왔다.	프갤러(110.8)	22:37	10	0
2898998	홍준표 동상 근황	발명도둑잡기(118.216)	22:23	10	0
2898996	국정원에서 뭐할라하나? 개발자를뽑네 [4]	ㅇㅇ(220.86)	22:20	34	0
2898995	수은으로 금 만드는 기술 등장, 핵융합 활용도 미쳤네;;	발명도둑잡기(118.216)	22:20	9	0
2898993	진짜 Sea Of Love	발명도둑잡기(118.216)	22:07	9	0
2898992	옛날엔 채널 50개도 안되도 볼거 많았는데	타이밍뒷.통수한방(1.213)	22:07	10	0
2898991	쿠팡 존나게 뛰고 업소 가서 돈 다쓴 썰..	ㅇㅇ(118.235)	22:07	17	0
2898990	동학과 임진왜란 - 영남과 호남이 만나서 같이~	발명도둑잡기(118.216)	21:56	10	0
2898988	메모리 페이지 기본값 4KB가 만국 표준 아님? [3]	프갤러(49.165)	21:53	24	0
2898986	u+ 채널이 999개인데 ㄹㅇ 볼만한채널이없음 ㅋㅋㅋㅋㅋㅋㅋㅋ	타이밍뒷.통수한방(1.213)	21:42	13	0
2898985	맥 최초 운영 체제 이름이 좀 특이하네	프갤러(140.213)	21:30	32	0
2898984	'집 6채' 장동혁, 모두 8.5억?‥"실거래가 맞나?"	발명도둑잡기(118.216)	21:18	13	0
2898981	와 근데 학생코드 짜다보면 느끼는데 항상 너무 어렵게짜서	ㅆㅇㅆ(124.216)	21:15	30	0
2898980	캄보디아 범죄단지급 냥덩이 계정 털날 다가온다	발명도둑잡기(118.216)	21:14	14	0
2898978	졸리댱..	♥벼락부자냥덩♥	21:14	23	0
2898976	재형(Jaehyung) X 민수(Minsu) - Sea of Love	발명도둑잡기(118.216)	21:09	8	0
2898975	나도 프밍에 재능 있었으면 좋았겠지	프갤러(220.121)	21:02	30	0
2898974	김연경씨라는 배구선수 비호감아니냐? [5]	헬마스터	20:57	44	0
2898972	ʕ⁎⁎ʔ༄	♥벼락부자냥덩♥	20:55	18	0
2898971	개발자 취업난 맞노? [6]	프갤러(180.231)	20:54	67	0
2898970	ʕ••ʕ••ʔ••ʔ••ʕ••ʔ••ʕ	♥벼락부자냥덩♥	20:52	19	0
2898969	나는 살면서 지나간 날이 그립진 않던데 그리운 애들 많구만	ㅆㅇㅆ(124.216)	20:51	20	0
2898968	☆:.｡. o(≧▽≦)o .｡.:☆ [1]	♥벼락부자냥덩♥	20:50	15	0
2898967	개발은 진짜 타고난 지능 좋아야 하는 직업이네 [3]	프갤러(116.45)	20:42	74	0
2898965	손은 눈보다 빠르당 By 나님	♥벼락부자냥덩♥	20:36	15	0
2898964	웹디자인은 AI 떄문에 진짜 이미 멸망한 것 같은데	프갤러(220.70)	20:35	25	0
2898963	미국 망하면 한국 래퍼가 미국에서 널리 불릴 날 온다	발명도둑잡기(118.216)	20:34	11	0
2898960	인터럽트가 함수 실행이랑 똑같음 [1]	재현	20:20	13	0
2898959	노정현의 '쇼미' 본능...안철수·박형준·이언주 디스쇼	발명도둑잡기(118.216)	20:15	12	0
2898958	대학원 지원서 맥락에서 대단하다고 표현될 만한 수준	나르시	20:13	17	0
2898957	냥냥⭐+	♥벼락부자냥덩♥	20:10	13	0
2898956	은근히 좋은 노래 [3]	노력	20:08	29	0
2898955	MALAYSIA CHABOR 馬來西亞查某 Joyce Chu	발명도둑잡기(118.216)	20:05	10	0
2898950	세상. 그리고 나.	프갤러(110.8)	19:43	19	0
2898948	한 달 전에 여름이었는데 갑자기 겨울이 됐구나	발명도둑잡기(118.216)	19:39	14	0
2898947	저장용 [2]	♥벼락부자냥덩♥	19:36	22	0
2898946	나님 월 마일리지 100 근접 ㅇㅅㅇ [1]	♥벼락부자냥덩♥	19:28	27	0
2898945	기술면접 과제가 내가 전혀 써본 적 없는 언어로 나오네 ㅋㅋ [1]	ㅇㅇ	19:14	43	0
2898944	이제 사람 좀 빠지네. 호흡에 집중할 수 있겠어 [1]	프갤러(27.171)	19:10	36	0
2898943	가호-시작 [2]	발명도둑잡기(118.216)	19:00	32	0
2898942	부천역 bj들 내쫒는 분위기네	프갤러(211.210)	18:59	29	0
2898941	❤✨☀⭐⚡☘⛩나님 시작합니당⛩☘⚡⭐☀✨❤ [2]	♥벼락부자냥덩♥	18:57	23	0
2898940	Part of your world	발명도둑잡기(118.216)	18:57	10	0
2898939	호흡속에서 질소와 산소와 이산화탄소를 느낀다. [2]	프갤러(27.175)	18:55	25	1
2898938	스쿼트다. 근육의 힘을 키워 지하철 가속도를 버텨낸다.	프갤러(27.175)	18:52	16	0
2898936	내가 항상 자신감이 있는 이유 [2]	ㅆㅇㅆ(124.216)	18:39	57	0