ນີ້ແມ່ນຄໍາສັ່ງ alt-ergo ທີ່ສາມາດດໍາເນີນການໄດ້ໃນ OnWorks ຜູ້ໃຫ້ບໍລິການໂຮດຕິ້ງຟຣີໂດຍໃຊ້ຫນຶ່ງໃນຫຼາຍບ່ອນເຮັດວຽກອອນໄລນ໌ຂອງພວກເຮົາເຊັ່ນ Ubuntu Online, Fedora Online, Windows online emulator ຫຼື MAC OS online emulator
ໂຄງການ:
NAME
Alt-Ergo - ເປັນຕົວພິສູດທິດສະດີອັດຕະໂນມັດທີ່ອຸທິດຕົນເພື່ອການກວດສອບໂຄງການ
ສະຫຼຸບສັງລວມ
alt-ergo [ ທາງເລືອກໃນການ ] ເອກະສານ
ລາຍລະອຽດ
Alt-Ergo ແມ່ນການພິສູດທິດສະດີອັດຕະໂນມັດ. ມັນໃຊ້ເວລາເປັນວັດສະດຸປ້ອນ polymorphic arbitrary ແລະ
ສູດຄຳນວນຫຼາຍອັນທີ່ລຽງລຳດັບທຳອິດທີ່ຂຽນເປັນເຫດຜົນຄື syntax.
OPTIONS
-h ຊ່ວຍເຫຼືອ. ຈະໃຫ້ທ່ານບັນຊີລາຍຊື່ເຕັມຂອງທາງເລືອກແຖວຄໍາສັ່ງ.
ຕົວຢ່າງ
ທິດສະດີຂອງ arrays ທີ່ມີປະໂຫຍດທີ່ມີດັດສະນີຈໍານວນເຕັມ . ທິດສະດີນີ້ສະຫນອງປະເພດຂອງການກໍ່ສ້າງໃນ
('a,'b) farray ແລະ syntax ທີ່ສ້າງຂຶ້ນໃນຕົວເພື່ອຈັດການອາເຣ.
ສໍາລັບຕົວຢ່າງ, ປະເພດຂໍ້ມູນທີ່ບໍ່ມີຕົວຕົນໄດ້ແລະ t array ທີ່ເປັນປະໂຫຍດ (int,
tau) farray ປະກາດດັ່ງນີ້:
ປະເພດ tau
logic t : (int, tau) farray
ການສະແດງອອກ:
t[i] ໝາຍເຖິງຄ່າທີ່ເກັບໄວ້ໃນ t ໃນດັດຊະນີ i
t[i1<-v1,...,in<-vn] ໝາຍເຖິງ array ທີ່ເກັບຄ່າດຽວກັນກັບ t ສຳລັບທຸກໆອັນ.
index ຍົກເວັ້ນອາດຈະເປັນ i1, ...,in, ບ່ອນທີ່ມັນເກັບຄ່າ v1, ...,vn. ການສະແດງອອກນີ້
ເທົ່າກັບ ((t[i1<-v1])[i2<-v2])...[in<-vn].
ຕົວຢ່າງ.
t[0<-v][1<-w]
t[0<-v, 1<-w]
t[0<-v, 1<-w][1]
ທິດສະດີການນັບຈຳ ນວນ.
ສໍາລັບຕົວຢ່າງ, ປະເພດຂອງ enumeration t ກັບ constructors A, B, C ແມ່ນຖືກກໍານົດດັ່ງຕໍ່ໄປນີ້
:
ປະເພດ t = A | ຂ | ຄ
ຊຶ່ງຫມາຍຄວາມວ່າຄ່າທັງໝົດຂອງປະເພດ t ແມ່ນເທົ່າກັບ A, B ຫຼື C. ແລະທັງໝົດນັ້ນ
ຜູ້ກໍ່ສ້າງເຫຼົ່ານີ້ແມ່ນແຕກຕ່າງກັນ.
ທິດສະດີຂອງການບັນທຶກ polymorphic.
ຕົວຢ່າງເຊັ່ນ polymorphic record type 'at with two labels a and b of type 'a and
int ຕາມລໍາດັບແມ່ນຖືກກໍານົດດັ່ງຕໍ່ໄປນີ້:
type 'at = { a : 'a; b: int }
ການສະແດງອອກ { a = 4; b = 5 } ແລະ { r ກັບ b = 3} ຫມາຍເຖິງບັນທຶກ, ໃນຂະນະທີ່ຈຸດ
notation ra ແມ່ນໃຊ້ເພື່ອເຂົ້າເຖິງປ້າຍກຳກັບ.
Alt-Ergo (v. >= 0.95) ອະນຸຍາດໃຫ້ຜູ້ໃຊ້ສາມາດບັງຄັບປະເພດຂອງຄໍາທີ່ໃຊ້ syntax ໄດ້. :
. ຕົວຢ່າງຂ້າງລຸ່ມນີ້ສະແດງໃຫ້ເຫັນເຖິງການນໍາໃຊ້ຄຸນສົມບັດໃຫມ່ນີ້.
ພິມ 'ບັນຊີລາຍຊື່
logic nil : 'b list
logic f : 'c list -> int
ເປົ້າໝາຍ g1 : f(nil) = f(nil) (* ບໍ່ຖືກຕ້ອງເພາະວ່າສອງຕົວຢ່າງຂອງ nil ອາດຈະມີ.
ປະເພດທີ່ແຕກຕ່າງກັນ *)
ເປົ້າໝາຍ g2 : f(nil:'d list) = f(nil:'d list) (* valid *)
ENVIRONMENT ຄວາມຮັບຜິດຊອບ
ERGOLIB
ເສັ້ນທາງທາງເລືອກສໍາລັບຫ້ອງສະຫມຸດ Alt-Ergo
AUTHORS
Sylvain Conchon <[email protected]> ແລະ Evelyne Contejean <[email protected]>
ໃຊ້ alt-ergo ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net
