From Formal Specification to Property Based Test

'SPN'PSNBM4QFDT UP1SPQFSUZ#BTFE5FTUT .BTBUP0ICB !PICBSZF 3VCZ,BJHJ SVCZLBJHJ$

4QFBLFS 4NBSU#BOL *OD 4PGUXBSF&OHJOFFS&OHJOFFSJOH.BOBHFS .BTBUP0ICB !PICBSZF !PICBSZF

*OUSPEVDUJPO 'PSNBMTQFDJ fi DBUJPO 1SPQFSUZCBTFEUFTUJOH .BUIFNBUJDBMMZQSFDJTFEFTDSJQUJPOPG BTZTUFN`TCFIBWJPS XSJUUFOJOBGPSNBM MBOHVBHFXJUIBXFMMEF
fi OFETZOUBYBOE TFNBOUJDT 5FTUJOHBQQSPBDIXIFSFZPVEF fi OF HFOFSBMQSPQFSUJFTUIBUTIPVMEBMXBZT IPMEBOEBVUPNBUJDBMMZDIFDLUIFN BHBJOTUNBOZSBOEPNMZHFOFSBUFE JOQVUT 'PSNBMNFUIPETBSFUIFCSPBEFSTFUPGUFDIOJRVFTBOEQSPDFTTFTUIBUVTFTVDIGPSNBMTQFDJ fi DBUJPOT

*OUSPEVDUJPO .PUJWBUJPOBOEQSPCMFNTUBUFNFOU 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS
'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU 'VUVSFQPTTJCJMJUJFT 0VUMJOF

.PUJWBUJPOBOEQSPCMFNTUBUFNFOU

.PUJWBUJPOBOEQSPCMFNTUBUFNFOU 5XPUIJOHTBSFTUJMMJNQPSUBOUJOTPGUXBSFEFWFMPQNFOU (PPEPMEXPSL fl PX Specification Implementation Test WFSJGZ
XSJUF

.PUJWBUJPOBOEQSPCMFNTUBUFNFOU 5XPUIJOHTBSFTUJMMJNQPSUBOUJOTPGUXBSFEFWFMPQNFOU (PPEPMEXPSL fl PX Specification Implementation Test 4QFDJ
fi DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO 🤔*TUIJTTQFDJ fi DBUJPOWBMJE WFSJGZ XSJUF

.PUJWBUJPOBOEQSPCMFNTUBUFNFOU 5XPUIJOHTBSFTUJMMJNQPSUBOUJOTPGUXBSFEFWFMPQNFOU (PPEPMEXPSL fl PX Specification Implementation Test *NQMFNFOUBUJPOTWFSJ
fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT 🤔$BOUFTUWFSJGZ 4QFDJ fi DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO 🤔*TUIJTTQFDJ fi DBUJPOWBMJE WFSJGZ XSJUF

.PUJWBUJPOBOEQSPCMFNTUBUFNFOU *OUIFBHFPG"*BTTJTUFEDPEFHFOFSBUJPO UIFZHFUNPSFJNQPSUBOU &WPMWJOHXPSL fl PX Implementation Test 4QFDJ
fi DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT 🤔*TUIJTTQFDJ fi DBUJPOWBMJE 🤔$BOUFTUWFSJGZ WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF Specification

fi DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT 🤔*TUIJTTQFDJ fi DBUJPOWBMJE 🤔$BOUFTUWFSJGZ WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF Specification *GTQFDJTCBE UIFHFOFSBUFE DPEFXJMMCFCBEUPP

fi DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT 🤔*TUIJTTQFDJ fi DBUJPOWBMJE 🤔$BOUFTUWFSJGZ WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF Specification *GTQFDJTCBE UIFHFOFSBUFE DPEFXJMMCFCBEUPP *GUFTUTGBJMUPQSPQFSMZWFSJGZUIF JNQMFNFOUBUJPO CVHTXJMMCF TIJQQFEUPQSPEVDUJPO

fi DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT 🤔*TUIJTTQFDJ fi DBUJPOWBMJE 🤔$BOUFTUWFSJGZ WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF Specification *GTQFDJTCBE UIFHFOFSBUFE DPEFXJMMCFCBEUPP *GUFTUTGBJMUPQSPQFSMZWFSJGZUIF JNQMFNFOUBUJPO CVHTXJMMCF TIJQQFEUPQSPEVDUJPO )PXDBOXFNBLF PVSEFWFMPQNFOUMJGFDZDMFCFUUFS

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH 8IZUIFZNBUUFS

'PSNBMNFUIPET

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS 'PSNBMNFUIPET w .BUIFNBUJDBMMZCBTFEUFDIOJRVFT GPSTQFDJGZJOH EFTJHOJOH BOE
WFSJGZJOHTPGUXBSFBOEIBSEXBSF TZTUFNT w 'PSNBMTQFDJ fi DBUJPOTBSFXSJUUFO JOBQSPHSBNNBUJDMBOHVBHF OPU OBUVSBMMBOHVBHF 8IBUJUHJWFTZPV ✅%FUFDUDPOUSBEJDUJPOT ✅&YIBVTUJWFTUBUFTFBSDI ✅"VUPDPVOUFSFYBNQMFT &YBNQMFT"MMPZ 5-" 2VJOU 'J[[#FF 6TFECZ"84 "NB[PO .POHP%# $MPVE fl BSF

'PSNBMTQFDJ fi DBUJPO 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS w 'PSNBMTQFDIBTDPODSFUF TUSVDUVSFTBOE
EFDMBSBUJPOTPGQSPQFSUJFT w 6OMJLFBNCJHVPVT OBUVSBMMBOHVBHF sig Element {} sig Stack { elements: seq Element } pred PushAddsElement[s, s': Stack, e: Element] { #s'.elements = add[#s.elements, 1] } pred PopRemovesElement[s, s': Stack] { #s.elements > 0 implies #s'.elements = sub[#s.elements, 1] } assert StackProperties { all s, s': Stack, e: Element | PushAddsElement[s, s', e] and (not IsEmpty[s] implies PopRemovesElement[s, s']) }

8IZGPSNBMTQFDNBUUFS 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS w 'PSNBMTQFDTDBUDIFSSPSTCFGPSFBOZDPEFJTXSJUUFO w "MMPZ 5-"
BOE2VJOUMFUZPVWFSJGZSFRVJSFNFOUTNBUIFNBUJDBMMZBUUIFTQFD TUBHF OPUBGUFSEFQMPZNFOU w .PEFMCBTFEUFTUJOH .#5 UBLFTJUGVSUIFS w %FSJWFWBMJETUBUFUSBOTJUJPOUSBDFTGSPNUIFNPEFMBOEVTFUIFNBTUFTUPSBDMFT w --.TSFBEQSPNQUT CVUQSPNQUTIJEFDPOUSBEJDUJPOT w /BUVSBMMBOHVBHFJOUFOUMFBWFTSPPNGPSNJTJOUFSQSFUBUJPO BOEJODPOTJTUFODJFT JOUIFTQFDJUTFMGBSFIBSEUPTQPU

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS *OUIFBHFPG"*BTTJTUFEDPEFHFOFSBUJPO UIFZHFUNPSFJNQPSUBOU &WPMWJOHXPSL fl PX Implementation
Test 4QFDJ fi DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT 🤔*TUIJTTQFDJ fi DBUJPOWBMJE 🤔$BOUFTUWFSJGZ WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF Specification

Implementation Test &WPMWJOHXPSL fl PX 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS *OUIFBHFPG"*BTTJTUFEDPEFHFOFSBUJPO
UIFZHFUNPSFJNQPSUBOU 4QFDJ fi DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT ✅7FSJ fi BCMFTQFD 🤔$BOUFTUWFSJGZ WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF Formal spec

1SPQFSUZCBTFEUFTUJOH

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS w 7FSJGZVOJWFSTBMQSPQFSUJFT JOTUFBEPGUFTUJOHJOEJWJEVBM FYBNQMFT w (FOFSBUFIVOESFET
UIPVTBOETPGUFTUJOQVUTBU SBOEPN w %FTDSJCFUFTUUBSHFUT QSPQFSUZ OPUBOFYBNQMF 3BOEPNJTO`USFBMMZSBOEPN$POUSPMMFEBOESFQSPEVDJCMFSBOEPNOFTT *OUIJTTMJEF *TPNFUJNFTVTF1#5BTBOBDSPOZNPGQSPQFSUZCBTFEUFTUJOH 1SPQFSUZCBTFEUFTUJOH

✅&BTZUPXSJUFBOEVOEFSTUBOE ✅6TFGVMUPFOTVSFPVSQSPHSBNXPSLT BTFYQFDUFE ❌ 0OMZ fi OETCVHTUIBUBQSPHSBNNFS QSFEJDUFE &YBNQMFCBTFEUFTUJOH
'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS 5IBUTPOFPGUIFNPUJWBUJPOTPG QSPQFSUZCBTFEUFTUJOH

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS %FNPIUUQTZPVUVCF,98SBLB:T

#FOF fi UTPGQSPQFSUZCBTFEUFTUJOH 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS ✅$BOUFTUNPSFJOQVUT ✅$BOUFTUNPSFEJWFSTFJOQVUT ✅$BOF
ff PSUMFTTMZ fi OE DPVOUFSFYBNQMFT

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS 4UBUFGVM1#5UFTUJOHTUBUFNBDIJOFT (FOFSBUFSBOEPNDPNNBOE TFRVFODFT 7FSJGZTUBUFNBUDIFTBU FWFSZTUFQ
.PEFM BCTUSBDU state: [] state: [3] state: [] push(3) 465 SFBM Stack.new Stack Stack WFSJGZ WFSJGZ WFSJGZ $BMMFEUSBDFTJOGPSNBMNFUIPET 465TUBOETGPSTZTUFNVOEFSUFTU pop push(3) pop

1SPQFSUZCBTFEUFTUJOHJO3VCZ 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS w *DSFBUFEBHFNUPXSJUF1#5 JOSVCZBOEQSFTFOUFEJO 3VCZ,BJHJ w
'PSGVUVSFSFGFSFODF TFFUIF TMJEFTPSWJEFP IUUQTTQFBLFSEFDLDPNPICBSZFVOMPDLJOHQPUFOUJBMPGQSPQFSUZCBTFEUFTUJOHXJUISBDUPS IUUQTXXXZPVUVCFDPNXBUDI W6MKK.R06* IUUQTHJUIVCDPNPICBSZFQCU

8IZQSPQFSUZCBTFEUFTUJOHNBUUFST 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS w 5IFJNQPSUBODFPGUFTUIBSOFTTFT BOEPSBDMFTJTHSPXJOHFTQFDJBMMZ XIFOXPSLJOHXJUI"*DPEJOHBHFOUT w
1SPQFSUZCBTFEUFTUJOHDBOQSPWJEF BTUSPOHFSIBSOFTTUIBOFYBNQMF CBTFEUFTUJOH w #FDBVTFJUWFSJ fi FTNBUIFNBUJDBM QSPQFSUJFTUIBUBGVODUJPONVTU BMXBZTTBUJTGZ it do result = sort([42,9,-1]) expect(result).to eq [-1,9,42] end def sort(array) [-1,9,42] end %POF 8SJUFBTPSUBMHPSJUINUPQBTTUIFUFTU

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS *OUIFBHFPG"*BTTJTUFEDPEFHFOFSBUJPO UIFZHFUNPSFJNQPSUBOU Implementation Test 4QFDJ fi
DBUJPODPSSFDUOFTT 1 XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT 🤔*TUIJTTQFDJ fi DBUJPOWBMJE 🤔$BOUFTUWFSJGZ WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF Specification &WPMWJOHXPSL fl PX

&WPMWJOHXPSL fl PX 1 Specification Implementation 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS
*OUIFBHFPG"*BTTJTUFEDPEFHFOFSBUJPO UIFZHFUNPSFJNQPSUBOU 4QFDJ fi DBUJPODPSSFDUOFTT XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF 🤔*TUIJTTQFDJ fi DBUJPOWBMJE ✅.VDINPSFWFSJ fi BCMF Property based tests

8IBUJGXFDPNCJOFUIFN

1 Implementation 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS 4PGUXBSFEFWFMPQNFOUXPSL fl PXXJUIWFSJ fi
DBUJPOT 4QFDJ fi DBUJPODPSSFDUOFTT XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF ✅.VDINPSFWFSJ fi BCMF Property based tests ✅7FSJ fi BCMFTQFD Formal spec 3PCVTUXPSL fl PX

1 Implementation 'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS 4PGUXBSFEFWFMPQNFOUXPSL fl PXXJUIWFSJ fi
DBUJPOT 4QFDJ fi DBUJPODPSSFDUOFTT XSJUJOHVOBNCJHVPVTTQFDJ fi DBUJPOTUIBUFMJNJOBUF SPPNGPSNJTJOUFSQSFUBUJPO *NQMFNFOUBUJPOTWFSJ fi DBUJPO 2 WFSJGZJOHUIBUJNQMFNFOUBUJPOTBDUVBMMZTBUJTGZUIPTF TQFDJ fi DBUJPOT WFSJGZ HJWFJOUFOU EJSFDUMZPSWJBTQFDT XSJUF ✅.VDINPSFWFSJ fi BCMF Property based tests ✅7FSJ fi BCMFTQFD Formal spec 🤔 3FMJBCMF 3PCVTUXPSL fl PX

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS 1#5TIPVMECFEFUFSNJOJTUJDBMMZCBTFEPOGPSNBMTQFDT Implementation Property based tests HFOFSBUF
XSJUF ✅WFSJGZ ✅WFSJGZ XSJUF Formal spec SFBE

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS 1#5TIPVMECFEFUFSNJOJTUJDBMMZCBTFEPOGPSNBMTQFDT Implementation Property based tests HFOFSBUF
XSJUF ✅WFSJGZ ✅WFSJGZ XSJUF Formal spec SFBE 7FSJ fi FETQFD 1 (FOFSBUFE1#5UPWFSJGZJNQMFNFOUBUJPO 2 "VUPOPNPVTDPEJOHBHFOU 3 #FUUFSRVBMJUZBTTVSBODF

'PSNBMTQFDT QSPQFSUZCBTFEUFTUJOH XIZUIFZNBUUFS 4PGUXBSFEFWFMPQNFOUXPSL fl PXXJUIWFSJ fi DBUJPOT Implementation
Property based tests 7FSJ fi FETQFD 1 (FOFSBUFE1#5UPWFSJGZJNQMFNFOUBUJPO 2 XSJUF ✅WFSJGZ ✅WFSJGZ XSJUF Formal spec SFBE "VUPOPNPVTDPEJOHBHFOU 3 #FUUFSRVBMJUZBTTVSBODF %FUFSNJOJTUJDBMMZ HFOFSBUF .JTTJOHQJFDFJTUIFCSJEHFCFUXFFOUIFN

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU *OQVU TQFDUPQCU "MMPZ BMT 2VJOU ROU @QCUSCTDB ff
PME @QCU@DPO fi HSCUFNQMBUF 0VUQVU 1BSTFTGPSNBMTQFDT FYUSBDUTTUSVDUVSBMQBUUFSOT HFOFSBUFTTUBUFGVM1#5TDB ff PMETGPS3VCZ TQFDUPQCU 'SPOUFOE "OBMZ[FS (FOFSBUPS Property based tests Formal spec IUUQTHJUIVCDPNPICBSZFTQFDUPQCU

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU -JWFEFNP %FNPIUUQTZPVUVCFHLCIT*,Q5(:

*OUFSOBMEFTJHO

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU *OQVU "MMPZ"EBQUFS "OBMZTJT 4UBUFGVM1SFEJDBUF"OBMZTJT (FOFSBUJPO 4UBUFGVM(FOFSBUPS $PSF4QFD%PDVNFOU "MMPZ
BMT 2VJOU ROU 2VJOU"EBQUFS 4UBUFGVM1SFEJDBUF"OBMZ[FS (VBSE*OGFSFODFS 4UBUF6QEBUF*OGFSFODFS 3FMBUFE)JOU"OBMZ[FS @QCUSCTDB ff PME @QCU@DPO fi HSCUFNQMBUF 'SPOUFOE 0VUQVU MBZFSTBSDIJUFDUVSF

%FTJHOEFDJTJPOT

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU EFTJHOEFDJTJPOT 1 2 3 4 4DB ff PME
OPUDPNQJMFS 3FHFOFSBUJPOTBGFPVUQVU 'JYVQTUSFBN OPUXPSLBSPVOET 1BUUFSOBOBMZTJTBOEQSPNPUJPO *OUFSGBDFDPODFSOT *OUFSOBMDPODFSOT

4DB ff PME OPUDPNQJMFS 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU w #VJMEBDPNQJMFSUIBUGVMMZ QSFTFSWFTUIFTFNBOUJDT PGUIFGPSNBMTQFDBOE
BVUPHFOFSBUFTDPNQMFUF UFTUT 1 w 4BGFTUSVDUVSBMJOGFSFODF GPSXIBUXFDBO FYQMJDJU DPO fi HCPVOEBSZGPSXIBU XFDBOOPU w 8PSTUDBTFJTKVTU50%0 5FNQUBUJPO 8IBU*DIPPTF ➡

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU 'PSNBMTQFDTBZT 3VCZOFFET 4UBUFTIBQF #s'.elements = add[ ... ]
state + [args] (VBSE #s.elements > 0 implies !state.empty? "SHUZQF e: Element Pbt.integer "1*NFUIPE (not specified) sut.push(element) 0CTFSWBUJPO (not specified) sut.to_a 4FNBOUJDHBQT'PSNBMTQFDTBZT8)"5 3VCZOFFET)08 g a p s

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU )PXPUIFSTCSJEHFUIFHBQJO.PEFMCBTFEUFTUJOH 5IPTFCMVFHSPVQTBSFCBTFEPO"5BYPOPNZPG.PEFM#BTFE5FTUJOH"QQSPBDIFT 6UUJOH 1SFUTDIOFS-FHFBSE 1 2
3 4 5 .BOVBM 3BOEPN4FBSDICBTFE )VNBOTIBOEXSJUFBMMNPEFMTBOE QSPQFSUJFT5IFUPPMPOMZIBOEMFT FYQMPSBUJPO TISJOLJOH BOEFYFDVUJPO 4DB ff PMEJOH4VQQPSU FH(SBQI8BMLFS TQFDUPQCU .PEFMDIFDLJOH "NPEFMDIFDLFSPSEFEJDBUFEFOHJOF FYQMPSFTUIFTUBUFTQBDFUPHFOFSBUF USBDFTBOEUFTUTFRVFODFT 4"5$POTUSBJOUTPMWJOH FH5FTU&SB "6OJU "VUPNBUFE )VNBOIBOEXSJUFTBMM 5IFTPMWFSEJSFDUMZTPMWFTDPOTUSBJOUTJO UIFTQFDUPEFSJWFUFTUDBTFT)VNBOT POMZXSJUFUIFTQFD FH"QBMBDIF 2VJDL4USPN 4QFD&YQMPSFS FH&DIJEOB 2VWJR2VJDL$IFDL ? "*BTTJTUFE FH"NB[PO,JSP

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU "OBMZTJT 4UBUFGVM1SFEJDBUF"OBMZTJT (FOFSBUJPO 4UBUFGVM(FOFSBUPS 4UBUFGVM1SFEJDBUF"OBMZ[FS (VBSE*OGFSFODFS 4UBUF6QEBUF*OGFSFODFS 3FMBUFE)JOU"OBMZ[FS
@QCUSCTDB ff PME @QCU@DPO fi HSCUFNQMBUF 0VUQVU MBZFSTBSDIJUFDUVSF *OQVU "MMPZ"EBQUFS "MMPZ BMT 2VJOU ROU 2VJOU"EBQUFS 'SPOUFOE 'SPOUFOEOFVUSBMJUZ 4BNFJEFBBTTFQBSBUJOH UIFGSPOUFOEBOECBDLFOEJODPNQJMFSEFTJHO 1BSTF"MMPZXJUIPXOSFHFYQBSTFS 2VJOUQBSTFS !JOGPSNBMTZTUFNTRVJOU $PSF4QFD%PDVNFOU

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU *OQVU "MMPZ"EBQUFS "OBMZTJT 4UBUFGVM1SFEJDBUF"OBMZTJT (FOFSBUJPO 4UBUFGVM(FOFSBUPS $PSF4QFD%PDVNFOU "MMPZ
BMT 2VJOU ROU 2VJOU"EBQUFS 4UBUFGVM1SFEJDBUF"OBMZ[FS (VBSE*OGFSFODFS 4UBUF6QEBUF*OGFSFODFS 3FMBUFE)JOU"OBMZ[FS 'SPOUFOE 8IBUTQFDUPQCUHFOFSBUFT @QCUSCTDB ff PME @QCU@DPO fi HSCUFNQMBUF 0VUQVU (FOFSBUFETDB ff PME PWFSXSJUUFOPOSFHFOFSBUJPO $PO fi HUFNQMBUF VTFSFEJUT QSFTFSWFE

3FHFOFSBUJPOTBGFPVUQVU 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU 2 #BEEFTJHO @QCUSC (FOFSBUF &EJU 3FHFOFSBUF &EJUTMPTU

3FHFOFSBUJPOTBGFPVUQVU 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU 2 #FUUFSEFTJHO (FOFSBUF fi MFT &EJUDPO fi
HPOMZ 3FHFOFSBUFUFTUPOMZ QSFTFSWFDPO fi H @QCUSC @QCU@DPO fi HSC

fi MFTFQBSBUJPO DPO fi H)BTI 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU @QCUSC $-*HFOFSBUFT
PWFSXSJUUFO SC 6TFSDSFBUFT JNQMFNFOUBUJPO 465 @QCU@DPO fi HSC $-*UFNQMBUFT VTFSFEJUT class Stack def initialize = @values = [] def push(value) @values << value nil end def pop = @values.pop def snapshot = @values.dup end

fi MFTFQBSBUJPO DPO fi H)BTI 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU @QCUSC $-*HFOFSBUFT
PWFSXSJUUFO StackPbtConfig = { sut_factory: -> { Stack.new }, command_mappings: { push: { method: :push } }, verify_context: { state_reader: -> (s) { s.to_a } } } @QCU@DPO fi HSC $-*UFNQMBUFT VTFSFEJUT Pbt.assert do Pbt.property(Pbt.array(Pbt.integer)) do output = stack(it) raise unless it.length = = output.length end end SC 6TFSDSFBUFT JNQMFNFOUBUJPO 465 5IF1#5UFTUJTQTFVEP"DUVBMUFTUDPEFJTNPSFDPNQMJDBUFECFDBVTFJUEZOBNJDBMMZMPBETUIFDPO fi HBOECVJME UFTUT /PUFEJUBCMF &EJUBCMF

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU w TQFDUPQCUHFOFSBUFTUFTUTVTJOHQCU HFN w "EEFEPbt.statefulUPQCUHFNGPS TQFDUPQCU w $PNNBOECBTFENPEFM465QBSBMMFM
FYFDVUJPO w &YUFOEFEQCUQSPUPDPMCFDBVTF3FBM EPNBJOTFYQPTFEQSPUPDPMMJNJUT 'JYVQTUSFBN OPUXPSLBSPVOET 3 Pbt.assert(seed: 2, num_runs: 1) do Pbt.stateful( model: PassingCounterModel.new, sut: -> { Object.new }, max_steps: 5 ) end

'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU *OQVU "MMPZ"EBQUFS (FOFSBUJPO 4UBUFGVM(FOFSBUPS "MMPZ BMT 2VJOU ROU
2VJOU"EBQUFS 'SPOUFOE @QCUSCTDB ff PME @QCU@DPO fi HSCUFNQMBUF 0VUQVU "OBMZTJT 4UBUFGVM1SFEJDBUF"OBMZTJT $PSF4QFD%PDVNFOU 4UBUFGVM1SFEJDBUF"OBMZ[FS (VBSE*OGFSFODFS 4UBUF6QEBUF*OGFSFODFS 3FMBUFE)JOU"OBMZ[FS

1BUUFSOBOBMZTJTBOEQSPNPUJPO 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU 4 w 5IFSFBSFTFNBOUJD HBQTCFUXFFO NPEFMBOE JNQMFNFOUBUJPO w
TQFDUPQCUUSJFTUP BOBMZ[FUIFTQFD BOEGVM fi MMUIFHBQ 'PSNBMTQFDTBZT 3VCZOFFET #s'.elements = add[ ... ] state + [args] (not specified) sut.push(element) (not specified) sut.to_a %JTDPWFSQBUUFSOTGSPNSFBMXPSMEMJLFFYBNQMFT

&YBNQMFDPOOFDUJPOQPPM 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU $IFDLPVUJTOFWFSJOUFSQSFUFE4USVDUVSFBMPOFJTFOPVHI pred Checkout[p, p': Pool] { #p.available
> 0 implies #p'.available = sub[#p.available, 1] and #p'.checked_out = add[#p.checked_out, 1] } available: decrement (-1) checked_out: increment (+1) shape: paired_counter guard: positive (> 0) "OBMZTJT $PSF4QFD%PDVNFOU 4UBUFGVM1SFEJDBUF"OBMZ[FS 4QFD "OBMZTJT

1BUUFSOTQSPNPUFUPBVUPHFOFSBUJPOXIFOBQBUUFSONFFUTUIFDPOEJUJPOT 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU ✅"QQFBSTJO EJ ff FSFOUEPNBJOT /PUBPOFP ff DPJODJEFODF
✅4USVDUVSBMMZJOGFSBCMFGSPNTQFDCPEZ /PEPNBJOLOPXMFEHFOFFEFE ✅4BGFEFGBVMUCFIBWJPS 8SPOHJOGFSFODFEPFTOUCSFBLUFTUT ✅"DUVBMMZSFEVDFTDPO fi HXPSL /PUKVTUNPWJOHMPHJDBSPVOE ✅3FHSFTTJPODPWFSBHFNBJOUBJOFE &YJTUJOHUFTUTTUJMMQBTT

1BUUFSOQSPNPUJPOTVDDFTTWTSFKFDUJPO 'SPNGPSNBMTQFDTUPQSPQFSUZCBTFEUFTU available: decrement (-1) checked_out: increment (+1) 4FFOJOconnection_pool,
hold_capture_release, transfer "MMDPOEJUJPOTNFU ✅1SPNPUFEQBJSFE@DPVOUFS ❌3FKFDUFECVTJOFTTSVMFQBUIT captured -> refund allowed 4UBUVTWBMVFTBSFEPNBJOTQFDJ fi D 8SPOHDIFDLCFDPNFTGBMTF QPTJUJWF 4UBZTDPO fi HPXOFE /PUDBO*BVUPNBUFJU CVUDBO*TBGFMZHFOFSBMJ[FJU *UFTUFEGPS SFBMXPSMEMJLFEPNBJOTBTMJLFUIFSJHIUDPMVNO

OPUDPNQJMFS 3FHFOFSBUJPOTBGFPVUQVU 'JYVQTUSFBN OPUXPSLBSPVOET 1BUUFSOBOBMZTJTBOEQSPNPUJPO *OUFSGBDFDPODFSOT *OUFSOBMDPODFSOT BOENPSF

'VUVSFQPTTJCJMJUJFT

'VUVSFQPTTJCJMJUJFT w 3FDPHOJ[FTLOPXOQBUUFSOT w 4UBUFGVM1#5POMZ w (FOFSBUFEDPEFJTOPUSFBEBCMF w 3FHFYQBSTFSDPWFSTdPG
"MMPZTZOUBY $VSSFOUMJNJUBUJPOT 5IFQBUIGPSXBSE w &YQBOEQBUUFSODBUBMPH w 4UBUFMFTT1#5TVQQPSU w 4JNQMJGZHFOFSBUJPOUFNQMBUFT w "MMPZ"OBMZ[FS"45GPSEFFQFS QBSTJOH ➡

'VUVSFQPTTJCJMJUJFT 8FDBONBLFTPGUXBSFEFWFMPQNFOUCFUUFS Implementation Property based tests 7FSJ fi FETQFD
1 (FOFSBUFE1#5UPWFSJGZJNQMFNFOUBUJPO 2 HFOFSBUF XSJUF ✅WFSJGZ ✅WFSJGZ XSJUF Formal spec SFBE "VUPOPNPVTDPEJOHBHFOU 3 #FUUFSRVBMJUZBTTVSBODF TQFDUPQCU

From Formal Specs to Property Based Tests Masato Ohba (@ohbarye)
RubyKaigi 2026 2026-04-23 #rubykaigiC

"QQFOEJY

3FGFSFODFT1SPQFSUZCBTFEUFTUJOH w 5FTUJOH"TZODISPOPVT"1*T8JUI2VJDL$IFDL w IUUQTXXXFSMBOHGBDUPSZDPNTUBUJDVQMPBENFEJBQCUFSMBOHGBDUPSZQQUYQEG w 2VJDL$IFDL"4JMWFS#VMMFUGPSUFTUJOH w
IUUQTIUNMQSFWJFXHJUIVCJP IUUQTSBXHJUIVCDPNTUSBOHFMPPQMBNCEBKBNNBTUFSTMJEFT/PSUPO 2VJDL$IFDLIUNM w *OUSPEVDUJPOUP1SPQFSUZ#BTFE5FTUJOH w IUUQTNFEJVNDPNDSJUFPFOHJOFFSJOHJOUSPEVDUJPOUPQSPQFSUZCBTFEUFTUJOHGE w 1SPQFSUZCBTFEUFTUJOHPGQSJWJMFHFEQSPHSBNT w IUUQTJFFFYQMPSFJFFFPSHEPDVNFOU w 1SPQFSUZCBTFEUFTUJOHBOFXBQQSPBDIUPUFTUJOHGPSBTTVSBODF w IUUQTEMBDNPSHEPJBCT w 2VJDL$IFDLBMJHIUXFJHIUUPPMGPSSBOEPNUFTUJOHPG)BTLFMMQSPHSBNT w IUUQTEMBDNPSHEPJ w 1SPQFSUZ#BTFE5FTUJOHXJUI1SPQ&S &SMBOH BOE&MJYJS w IUUQTQSBHQSPHDPNUJUMFTGIQSPQFSQSPQFSUZCBTFEUFTUJOHXJUIQSPQFSFSMBOHBOEFMJYJS

3FGFSFODFT'PSNBMNFUIPET w "MMPZ"OBMZ[FS %BOJFM+BDLTPO .*5 w IUUQTBMMPZUPPMTPSH w
4PGUXBSF"CTUSBDUJPOT %BOJFM+BDLTPO .*51SFTT w "MMPZJUTBCPVU5JNF )JMMFM8BZOF w IUUQTXXXIJMMFMXBZOFDPNQPTUBMMPZ w "QQMJDBUJPOTBOEFYUFOTJPOTPG"MMPZQBTU QSFTFOUBOEGVUVSF w IUUQTXXXDBNCSJEHFPSHDPSFKPVSOBMTNBUIFNBUJDBMTUSVDUVSFTJODPNQVUFSTDJFODFBSUJDMFBQQMJDBUJPOTBOE FYUFOTJPOTPGBMMPZQBTUQSFTFOUBOEGVUVSF'$#'""$&#"$$ w 4QFDJGZJOH4ZTUFNT -FTMJF-BNQPSU w IUUQTMBNQPSUB[VSFXFCTJUFTOFUUMBCPPLQEG w 5-" JO1SBDUJDFBOE5IFPSZ1BSU w IUUQTQSPOHJUIVCJPQPTUTUMBQMVT@QBSU w $POGPSNBODF$IFDLJOH"U.POHP%# w IUUQTXXXNPOHPECDPNDPNQBOZCMPHFOHJOFFSJOHDPOGPSNBODFDIFDLJOHBUNPOHPECUFTUJOHPVSDPEF NBUDIFTPVSUMBTQFDT

3FGFSFODFT'PSNBMNFUIPET w 2VJOU *OGPSNBM4ZTUFNT w IUUQTRVJOUMBOHPSH w 3FMJBCMF4PGUXBSFJOUIF--.&SB
w IUUQTRVJOUMBOHPSHQPTUTMMN@FSB w .PEFM#BTFE5FTUJOH 2VJOUEPDT w IUUQTRVJOUMBOHPSHEPDTNPEFMCBTFEUFTUJOH w 'J[[#FF w IUUQT fi [[CFFJP w *OUSPEVDJOH'J[[#FF4JNQMJGZJOH'PSNBM.FUIPETGPS"MM 5IF/FX4UBDL w IUUQTUIFOFXTUBDLJPJOUSPEVDJOH fi [[CFFTJNQMJGZJOHGPSNBMNFUIPETGPSBMM w "845-" w IUUQTMBNQPSUB[VSFXFCTJUFTOFUUMBBNB[POFYDFSQUIUNM w .POHP%#5-" w IUUQTXXXNPOHPECDPNDPNQBOZCMPHFOHJOFFSJOHDPOGPSNBODFDIFDLJOHBUNPOHPECUFTUJOHPVSDPEFNBUDIFTPVSUMBTQFDT w $FEBS"/FX-BOHVBHFGPS"VUIPSJ[BUJPO "NB[PO '4& w IUUQTBTTFUTBNB[POTDJFODFBCDCEGFGDDBECDFEBSBOFXMBOHVBHFGPSFYQSFTTJWFGBTUTBGFBOEBOBMZ[BCMFBVUIPSJ[BUJPOQEG w )PX8F#VJMU$FEBS"7FSJ fi DBUJPO(VJEFE"QQSPBDI w IUUQTBSYJWPSHBCT

3FGFSFODFT.PEFM#BTFE5FTUJOH4QFDUP5FTU(FOFSBUJPO w 5FTU&SB4QFDJ fi DBUJPOCBTFE5FTUJOHPG+BWB1SPHSBNT6TJOH4"5 ,IVSTIJE.BSJOPW "4& w
IUUQTVTFSTFDFVUFYBTFEVdLIVSTIJEQBQFST5FTU&SB"4&+QEG w "6OJU"VUPNBUFE5FTU(FOFSBUJPOBOE.VUBUJPO5FTUJOHGPS"MMPZ 8BOHFUBM *$45 w IUUQTLBJZVBOXHJUIVCJPQBQFSTQBQFSJDTUQEG w .PEFM#BTFE5FTUJOHXJUI5-" BOE"QBMBDIF ,VQSJBOPW,POOPW 5-" $POGFSFODF w IUUQTDPOGUMBQMVT,VQSJBOPW@BOE@,POOPW.PEFMCBTFE@UFTUJOH@XJUI@5-"@ @BOE@"QBMBDIFQEG w (SBQI8BMLFS w IUUQTHSBQIXBMLFSHJUIVCJP w 'VMMZ5FTUFEDPEFHFOFSBUJPOGSPN5-" TQFDJ fi DBUJPOT "$. w IUUQTEMBDNPSHEPJGVMM)UNM w .PEFM#BTFE5FTUJOH*OGPSNBM4ZTUFNT w IUUQTNCUJOGPSNBMTZTUFNTEPDTUMB@CBTJDT@UVUPSJBMTUVUPSJBMIUNM w .PEFM#BTFE5FTUJOH'SPN4QFDUP5FTUTXJUI2VJOU w IUUQTTFFRVJDLHJUIVCJPQPTUTNPEFMCBTFEUFTUJOHXJUIGPSNBMWFSJ fi DBUJPO w "5BYPOPNZPG.PEFM#BTFE5FTUJOH"QQSPBDIFT 6UUJOH 1SFUTDIOFS-FHFBSE w 'JOEJOH#VHTXJUI4QFDJ fi DBUJPO#BTFE5FTUJOHJT&BTZ w IUUQTBSYJWPSHBCT

3FGFSFODFT4UBUFGVMQSPQFSUZCBTFEUFTUJOH "* 1#5 w 2VWJR2VJDL$IFDL &SMBOH TUBUFNDBMMCBDLT )VHIFT -/$4
w )ZQPUIFTJTTUBUFGVMUFTUJOH 1ZUIPO w IUUQTIZQPUIFTJTSFBEUIFEPDTJPFOMBUFTUTUBUFGVMIUNM w &DIJEOBTNBSUDPOUSBDUGV[[FS (SJFDPFUBM *445" w IUUQTHJUIVCDPNDSZUJDFDIJEOB w 'PVOESZ4PMJEJUZUFTUJOH w IUUQTCPPLHFUGPVOESZTI w "HFOUJD1SPQFSUZ#BTFE5FTUJOH'JOEJOH#VHT"DSPTTUIF1ZUIPO&DPTZTUFN "OUISPQJD."54/PSUIFBTUFSO /FVS*14%-$ w IUUQTBSYJWPSHBCT w IUUQTHJUIVCDPNNNBB[HJUBHFOUJDQCU w "NB[PO,JSPTQFDESJWFODPEFHFOFSBUJPO w IUUQTLJSPEFW w IUUQTLJSPEFWCMPHQSPQFSUZCBTFEUFTUJOH w 6TF1SPQFSUZ#BTFE5FTUJOHUP#SJEHF--.$PEF(FOFSBUJPOBOE7BMJEBUJPO w IUUQTBSYJWPSHBCT w 6OEFSTUBOEJOHUIF$IBSBDUFSJTUJDTPG--.(FOFSBUFE1SPQFSUZ#BTFE5FTUT w IUUQTBSYJWPSHBCT

3FGFSFODFT"* GPSNBMNFUIPET w #FZPOE7JCF$PEJOH6TJOH5-" BOE&YFDVUBCMF4QFDJ fi DBUJPOTXJUI$MBVEF 4IBI#IBU
w IUUQTTIBICIBUNFEJVNDPNCFZPOEWJCFDPEJOHVTJOHUMBBOEFYFDVUBCMFTQFDJ fi DBUJPOTXJUI DMBVEFEGB ff w 5PXBSET-BOHVBHF.PEFM(VJEFE5-" 1SPPG"VUPNBUJPO w IUUQTBSYJWPSHBCT w 1SPQFSUZ(15--.ESJWFO'PSNBM7FSJ fi DBUJPOPG4NBSU$POUSBDUT /%44 w IUUQTXXXOETTTZNQPTJVNPSHOETTQBQFSQSPQFSUZHQUMMNESJWFOGPSNBMWFSJ fi DBUJPOPGTNBSU DPOUSBDUTUISPVHISFUSJFWBMBVHNFOUFEQSPQFSUZHFOFSBUJPO w 8IFO"*8SJUFTUIF8PSMET4PGUXBSF 8IP7FSJ fi FT*U -FPOBSEPEF.PVSB w IUUQTMFPEFNPVSBHJUIVCJPCMPHXIFOBJXSJUFTUIFXPSMETTPGUXBSFXIPWFSJ fi FTJU w #VJMESFMJBCMF"*TZTUFNTXJUI"VUPNBUFE3FBTPOJOHPO"NB[PO#FESPDL w IUUQTBXTBNB[PODPNCMPHTNBDIJOFMFBSOJOHCVJMESFMJBCMFBJTZTUFNTXJUIBVUPNBUFE SFBTPOJOHPOBNB[POCFESPDLQBSU

From Formal Specification to Property Based Test

From Formal Specification to Property Based Test

More Decks by Masato Ohba

Other Decks in Programming

Featured

Transcript