이 튜토리얼은 애니메이션 로제타(하이포트로코이드)를 SVG 파일로 생성하는 프로그램을 만들어 Ada의 기능을 보여줍니다. Ada 2022 기능을 사용하고 Ada의 패키지 관리자인 Alire를 사용하여 프로젝트를 관리합니다. 이 튜토리얼은 Ada의 가독성, 강력한 형식 지정 및 안전성에 중점을 두고 기하학적 계산 및 SVG 렌더링에서 Ada의 사용법을 보여줍니다. 저자는 Ada가 안전 중요 응용 프로그램으로 알려져 있음에도 불구하고 현대적인 범용 언어로 적합함을 강조합니다.
더 보기
증가하는 사이버 보안 위협에 대응하기 위해 NVIDIA 보안팀은 기존 테스트 방법을 버리고 SPARK를 이용한 형식적 검증을 채택했습니다. 단 3개월 만에 보안에 중요한 C 코드를 SPARK로 성공적으로 변환하여 성능 저하 없이 보안을 향상시킬 수 있음을 증명했습니다. 현재 50명 이상의 NVIDIA 개발자가 SPARK 교육을 이수했으며, 많은 제품에 SPARK 구성 요소가 탑재되어 있습니다. 이 사례 연구는 형식적 검증의 성공 사례이며, 보안 강화를 목표로 하는 다른 조직에 귀중한 교훈을 제공합니다.
더 보기
2024년 Ada/SPARK Crate of the Year Awards 결과가 발표되었습니다! Lionel Draghi는 자동 테스트를 위해 이해하기 쉬운 Markdown 형식의 동작 사양을 사용하는 명령줄 도구 BBT로 Ada Crate of the Year를 수상했습니다. Kevin Chadwick은 메모리 안전한 로깅 라이브러리 elogs(SPARK 실버 인증)로 SPARK Crate of the Year를 수상했습니다. 이 라이브러리는 사용자가 최대 메시지 길이를 지정할 수 있습니다. 마지막으로, Brent Seidel의 임베디드 가능한 Lisp 인터프리터 bbs_lisp가 Embedded Crate of the Year를 수상하며 임베디드 시스템에서 Ada의 강점을 보여주었습니다.
더 보기