sara lee (Apr 07 2022 at 18:32): sara lee (Apr 07 2022 at 18:32):I have formally verified model of a system. If someone/user don't want to go in details of this system and just want to see its response. For such person this model is a close box with one output and two inputs(of same type). User have a block of data ,whose datatype match with the input of close box. Now user pass two values (in sequence) from his data block to the close box and want to see the response of the system. Since box is verified therefore only link to this box is two inputs.I want to ask how to write it formally in Coq and which command i should apply. Please guide me.
Last updated: Oct 03 2023 at 21:01 UTC