SWIG를 사용하는 Maude 사양 언어에 대한 언어 바인딩. 이들은 바인딩을 통해 액세스할 수 있는 전략에 의해 제어되는 시스템에 대한 모델 검사기로 확장된 수정된 버전의 Maude를 사용합니다.
Python 패키지는 PyPI에서 사용할 수 있습니다. pip install maude
사용하여 설치한 후 Maude가 패키지에 포함되어 있으므로 직접 사용할 수 있습니다.
import maude
maude . init ()
nat = maude . getModule ( 'NAT' )
t = nat . parseTerm ( '1 + 2' )
t . reduce ()
print ( t )
SWIG에서 지원하는 다른 언어에 대한 바인딩은 이 저장소에서 구축할 수 있지만 구체적인 지원 및 테스트는 제공되지 않았습니다. 그 중 일부에 대한 구체적인 지침은 여기에서 확인할 수 있습니다.
이 저장소에는 Maude의 확장 버전이 하위 모듈로 포함되어 있으며, 먼저 git submodule update --init
또는 이에 상응하는 Git 명령을 사용하여 복제해야 합니다. Python 패키지를 빌드하려면 다음 표준 명령을 통해 scikit-build-core를 사용합니다.
python -m build # or
pip wheel .
이로 인해 저장소에 설명된 대로 Meson 빌드 시스템, Ninja 및 다양한 외부 라이브러리와 도구가 필요한 subprojects
디렉토리에 Maude가 빌드됩니다. 또는 라이브러리로 컴파일된 Maude 버전을 릴리스 섹션에서 다운로드하여 예상 위치에 배치할 수 있습니다.
subprojects/maudesmc/installdir/lib
config.h
헤더 파일에 대한 subprojects/maudesmc/build
이 경우 또는 하위 디렉터리에서 Maude를 직접 빌드하는 경우 이전 명령 앞에 CMAKE_ARGS="-DBUILD_LIBMAUDE=OFF"
추가해야 합니다.
다른 언어에 대한 바인딩은 CMake를 사용하여 직접 빌드할 수도 있습니다. 여기서 srcdir
은 저장소가 복제된 디렉터리이고 language
는 SWIG에서 지원하는 언어 중 하나입니다.
cmake <srcdir> -DLANGUAGE=<language>
cmake --build .
일부 언어 대상의 경우 이것으로 충분하지만 다른 언어 대상의 경우 추가 단계가 필요할 수 있습니다.
Python 패키지에 대한 문서는 여기에서 확인할 수 있으며, 이는 주로 다른 대상 언어로 추정될 수 있습니다. Javadoc에서 생성된 문서도 사용할 수 있습니다. 이 외에도 저장소의 예제를 다양한 주제에 대한 참조로 사용할 수 있습니다.
test.py
검색.match.py
에서 일치.apply.py
에서 선택적으로 규칙을 적용합니다.unify.py
에서 통합합니다.graph.py
에서 재작성 그래프를 조작합니다.modelcheck.py
에서 모델을 확인합니다.vunarrow.py
에서 범위를 좁힙니다.variants.py
의 변형 생성.gui.py
에서 용어의 인수를 반복합니다.buildTerm.py
의 기호로 용어를 작성합니다.maudedoc.py
에서 모듈을 검사합니다.loading.py
에 원시 텍스트를 입력합니다.metalevel.py
의 메타레벨 조작.hooks.py
의 사용자 정의 특수 연산자.또한 라이브러리에 대한 튜토리얼은 라이브러리로서의 Maude: 효율적인 다목적 프로그래밍 인터페이스 기사에서 디자인 및 구현에 대한 설명과 함께 제공됩니다.