이것은 Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 공급자에서 실행할 수 있는 cafeobj 명령입니다.
프로그램:
이름
cafeobj - 대수 사양 및 프로그래밍 언어
개요
카페오브젝트 [OPTION]... [파일] ...
기술
시작합니다 카페OBJ 통역사.
카페OBJ 많은 고급 형식을 계승하는 가장 진보된 형식 명세 언어입니다.
기능(예: 유연한 혼합 수정 구문, 순서가 있는 강력하고 명확한 타이핑 시스템
매개변수 인스턴스화를 위한 정렬, 매개변수 모듈 및 보기, 모듈
식 등) OBJ(또는 더 정확하게는 OBJ3) 대수 사양 언어에서.
CafeOBJ는 모델의 공식(예: 수학적) 사양을 작성하기 위한 언어입니다.
다양한 종류의 소프트웨어 및 시스템과 이들의 속성을 검증합니다. 카페OBJ
다시 작성하여 등식 논리를 구현하고 강력한 대화식 정리로 사용할 수 있습니다.
증명 시스템. 지정자는 CafeOBJ에서도 증명 점수를 작성할 수 있으며 다음을 통해 증명을 수행할 수 있습니다.
증명 점수를 실행합니다.
CafeOBJ는 기관에 기반한 최첨단의 엄격한 논리적 의미를 가지고 있습니다. 더카페OBJ
입방체는 다양한 논리 조합의 기본이 되는 다양한 논리의 구조를 보여줍니다.
언어에 의해 구현된 패러다임. CafeOBJ의 증명 점수도 다음을 기반으로 합니다.
엄격한 의미 체계를 기반으로 하며 완전한 증명 세트를 사용하여 구성할 수 있습니다.
규칙.
옵션
두 종류의 옵션이 있습니다. 첫 번째는 다음을 위한 옵션입니다. 카페오브젝트 래퍼 스크립트
기본 Common Lisp 인터프리터를 선택하고 검색 경로를 조정할 수 있습니다.
매개 변수를 설정합니다.
-엔진 이름
기본 공통 리스프 엔진을 선택합니다. 지정하지 않으면 가장 먼저 선택한
빌드 시간 동안 사용됩니다.
-목록 엔진
사용 가능한 모든 공통 리스프 엔진 나열
-래퍼-libpath PATH
LISP 인터프리터의 메모리 덤프가 있는 경로를 설정합니다.
-래퍼 공유 경로 PATH
CafeOBJ 초기화 파일이 검색되는 경로를 설정합니다.
다음 옵션 세트는 CafeOBJ 인터프리터에 직접 지정됩니다.
-도움 도움말 메시지 인쇄
-q 사용자의 초기화 파일을 로드하지 않음
-일괄 배치 모드로 실행
-p PATH
모듈을 정의하는 표준 prelude 파일을 제공합니다.
+p PATH
추가 서곡 파일 로드
-l 디렉터리 목록
콜론으로 구분된 모듈 검색 경로의 경로 이름 목록 설정
+l 디렉터리 목록
모듈 검색 경로에 대한 경로 이름 목록을 추가합니다.
파일 시작할 때 순서대로 로드되는 파일.
onworks.net 서비스를 사용하여 온라인에서 cafeobj 사용
