이 내가 원하는 것을 나타내지 만 이는 작동하지 않습니다구문 "F;"를 번역하고 싶습니다. "참 참 참 참"으로하고, "부울 목록"에서 사용하는
이syntax
"_F_hex" :: "any => any" ("F;")
translations
"F;" => "True,True,True,True"
이 같은 F;을 사용합니다 :
[F;,F;] == [True,True,True,True,True,True,True,True]
Isabelle은 번역의 오른쪽을 구문 분석 할 수 있어야하지만 True,True,...은 유효한 구문 트리를 생성하지 않습니다. 목록 열거 형에 대해서만 F;을 사용하면 목록 열거에 대한 구문 변환 규칙을 다음과 같이 확장 할 수 있습니다. 그 "유형"용어에 대한 파스 트리 노드를 의미합니다 (양식 _ => _의 무언가가 아니라) logic 그래서 _F_hex는 어떤 인수를하지 않는
syntax "_F_hex" :: "logic" ("F;")
translations
"[F;, xs]" => "CONST True # CONST True # CONST True # CONST True # [xs]"
"[F;]" => "CONST True # CONST True # CONST True # CONST True # []"
참고. 번역에서는 True과 같은 논리에 상수를 CONST으로 표시해야합니다. 그렇지 않으면 Isabelle은 True을 변수로 처리합니다.
Andreas, 다시 한 번 감사드립니다. 이제 Plug'n'play 액션. 중요 할 때 중요한 대답을하십시오. 몇 가지 재귀적인 번역을 정의하는 것을 우연히 만났지만이 것은 얻지 못했고 재귀 구문을 구현할 때 참조 할 중요한 예를 보여줄 것입니다. 다음은 관심을 가질만한 C 언어 검증 자입니다 : [VCC] (http://vcc.codeplex.com/). 나는 어제 그것을 발견했다. 얼마나 유용한 지 모르지만 Z3 검증기를 사용합니다. [HOL-Boogie] (http://isabelle.in.tum.de/repos/isabelle/file/4dd08fe126ba/src)와 관련된 이사벨입니다./HOL/SMT_Examples) –