Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations