MO
M.Z. Olszewski
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
1 records found
1
Bridging the Gap in Software Verification - Agda Proofs to Haskell Test Case Generators
How can preconditions in Agda be translated to a QuickCheck generator in Haskell?
Property-based testing is a popular testing paradigm, especially common in the functional programming language Haskell through the QuickCheck library. On the other hand, Agda is a dependently-typed language used as a proof assistant and for software verification. Because of the need for software verification, Agda2hs was created as a tool for translating code between these two, combining proven functionality with practical execution.
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics. ...
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics. ...
Property-based testing is a popular testing paradigm, especially common in the functional programming language Haskell through the QuickCheck library. On the other hand, Agda is a dependently-typed language used as a proof assistant and for software verification. Because of the need for software verification, Agda2hs was created as a tool for translating code between these two, combining proven functionality with practical execution.
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics.
This work explores making QuickCheck-compatible generators based on properties encoded in Agda. This should allow automating early checking of Agda proofs for correctness, as well as enabling conversion of formal specifications to executable tests for Haskell projects. A procedure is presented that permits creating advanced generators and checkers, and it is later evaluated in terms of multifaceted performance metrics.