From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,HTML_MESSAGE,MAILING_LIST_MULTI autolearn=ham autolearn_force=no version=3.4.4 Received: from minnie.tuhs.org (minnie.tuhs.org [50.116.15.146]) by inbox.vuxu.org (Postfix) with ESMTP id BA0A2215A2 for ; Sat, 25 May 2024 02:18:14 +0200 (CEST) Received: from minnie.tuhs.org (localhost [IPv6:::1]) by minnie.tuhs.org (Postfix) with ESMTP id 7423843680; Sat, 25 May 2024 10:18:10 +1000 (AEST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=tuhs.org; s=dkim; t=1716596290; h=from:from:reply-to:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type:in-reply-to:in-reply-to: references:references:list-id:list-help:list-owner:list-unsubscribe: list-subscribe:list-post; bh=rjR09k+ve2s5L74l4O+MWJ03qVJghSTAPUZGTQu2IUs=; b=sEr6NhxKxxsYw7oXELatQShwzR8cr/j3Jl9KCnx2RRaSdK+rRdRiIKGxWnokkh+yl1QHS+ Ewvq+UVvPD/luuge5OSzPF4wN1RM/cQ0uBJRuM2EeUVwDrzsHN2saskHT4dMYly6TFBAVN SZurjA5UHae1p1Y/MPh1aQOf3ravw1k= Received: from mail-pl1-x631.google.com (mail-pl1-x631.google.com [IPv6:2607:f8b0:4864:20::631]) by minnie.tuhs.org (Postfix) with ESMTPS id C5AE34367A for ; Sat, 25 May 2024 10:18:05 +1000 (AEST) Received: by mail-pl1-x631.google.com with SMTP id d9443c01a7336-1f3423646b7so20631865ad.0 for ; Fri, 24 May 2024 17:18:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=iitbombay-org.20230601.gappssmtp.com; s=20230601; t=1716596285; x=1717201085; darn=tuhs.org; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:from:to:cc:subject:date:message-id:reply-to; bh=rjR09k+ve2s5L74l4O+MWJ03qVJghSTAPUZGTQu2IUs=; b=DI9hWMd8mG94UYbTJggFSF3+e7n6KoRJNpcDq/Jw/QfbvMvYXdl7J6/+8xosDDgNcX SoMQ4FLYfO0MlfF4J7mi5qQfCi5wsHq7n9jlCWLePPyyYmVA/DVW5DKLVkrSXdMMDOdy mWMTRQ8pdOY1Fb7VS8z700qM81jixVqdVUO+nbNJePRZT9fU5jkyA6vfrEJ3psLT30QA Z3HDSS8MQGQNlJhPWGM0QGU4mJPEJC+EIxV8ctNC4WOZlP496PnbaU/ujKE8m6vuN9uv uW/d0Z5WVzSxTzw0nB2VE1YKuuQWQel+v/bHCb5/7BHxI2S9kEOYTjc3H37G2/8sF/VJ KfTA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1716596285; x=1717201085; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=rjR09k+ve2s5L74l4O+MWJ03qVJghSTAPUZGTQu2IUs=; b=KewyUJ9xTlkYQvbyoP4sJFq+fSLBVK8vy69hbHehoZjN5liyE/Q4e/r8jzvM8pZ8Jv BGF+mFDVurhh3cJ/2vtRSt+kZIr7DVvtNherjj3D9LClGiWAyDHQLoDPfPz5BmwsV7Z/ 8wLJPGojvSuQSL9fenEblEL4RLxngHSmnxdtW2SCQ6FMP7HrazbDHZecuxTNT4NGzfPZ yJ8lcbnzku9yOCt7Zz/pFRfQeqSVA1jmhppKQvMjZdLisog+L5hj/5u7absZHCqCgI3d 4EMzfIdz/n8iAlJkZsYFCw9hGBdj5lUGMOwvPw80nCOLlhjbbxYO+IyV7htp6mfEJTPT Hk2Q== X-Forwarded-Encrypted: i=1; AJvYcCWGNnNsByyXAbtZ0p9kkxy6IFUw+qWbtfcgviF7VrzUAc4JY0Ow7XQr46G1ZsyhvjU8Z5rpWmOG1Wjal8qb X-Gm-Message-State: AOJu0Yw4d1T86/Bjo0oelC4DZXu05EiCueApgZbilwmQ4gFTlemGsbQV KI5LKbdietI5HddfQYnqWbRbw5t+lwOb6A6RNgCj8wzAeeWES/ViFNiXBwmTiA== X-Google-Smtp-Source: AGHT+IEl4yz9cj1gdNAz0TX7vVVlBF6ILnEVFEhjQB8okfEUjqYM0rcmMbGdIAGZi6+F0B082IS8Kw== X-Received: by 2002:a17:902:e889:b0:1f4:6c83:23df with SMTP id d9443c01a7336-1f46c834745mr907845ad.33.1716596284867; Fri, 24 May 2024 17:18:04 -0700 (PDT) Received: from smtpclient.apple (107-215-223-229.lightspeed.sntcca.sbcglobal.net. [107.215.223.229]) by smtp.gmail.com with ESMTPSA id d9443c01a7336-1f44c9a9dabsm19576035ad.236.2024.05.24.17.18.03 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 24 May 2024 17:18:04 -0700 (PDT) Message-Id: <1E156D9B-C841-4693-BEA4-34C4BF42BCD5@iitbombay.org> Content-Type: multipart/alternative; boundary="Apple-Mail=_0E6664EE-78A1-4170-9120-208E5206B036" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3774.600.62\)) Date: Fri, 24 May 2024 17:17:53 -0700 In-Reply-To: To: Rob Pike References: X-Mailer: Apple Mail (2.3774.600.62) Message-ID-Hash: APQJ67UR7SMAY27ZCHRY45DA4ZRT3I2U X-Message-ID-Hash: APQJ67UR7SMAY27ZCHRY45DA4ZRT3I2U X-MailFrom: bakul@iitbombay.org X-Mailman-Rule-Misses: dmarc-mitigation; no-senders; approved; emergency; loop; banned-address; member-moderation; nonmember-moderation; administrivia; implicit-dest; max-recipients; max-size; news-moderation; no-subject; digests; suspicious-header CC: Douglas McIlroy , The Unix Heritage Society mailing list X-Mailman-Version: 3.3.6b1 Precedence: list Subject: [TUHS] Re: A fuzzy awk List-Id: The Unix Heritage Society mailing list Archived-At: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: From: Bakul Shah via TUHS Reply-To: Bakul Shah X-Spam: Yes --Apple-Mail=_0E6664EE-78A1-4170-9120-208E5206B036 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 What would be nice if programming languages provided some support for = such exhaustive testing[1]. At one point I had suggested turning Go's Interface type to something = like Guttag style abstract data types in that relevant axioms are = specified right in the interface definition. The idea was that any = concrete type that implements that interface must satisfy its axioms. = Even if the compiler ignored these axioms, one can write a support = program that can generate a set of comprehensive tests based on these = axioms. [Right now a type "implementing" an interface only needs to have = a set of methods that exactly match the interface methods but nothing = more] The underlying idea is that each type is in essence a constraint = on what values an instance of that type can take. So adding such axioms = simply tightens (& documents) these constraints. Just the process of = coming up with such axioms can improve the design (sor of like test = driven design but better!). Now it may be that applying this to anything more complex than stacks = won't work well & it won't be perfect but I thought this was worth = experimenting with. This would be like functional testing of all the = nuts and bolts and components that go in an airplane. The airplane may = still fall apart but that would be a "composition" error! [1] There are "proof assisant" or formal spec languages such as TLA+, = Coq, Isabelle etc. but they don't get used much by the average = programmer. I want something more retail! > On May 23, 2024, at 1:52=E2=80=AFPM, Rob Pike = wrote: >=20 > The semantic distinction is important but the end result is very = similar. "Fuzzing" as it is now called (for no reason I can intuit) = tries to get to the troublesome cases faster by a sort of depth-first = search, but exhaustive will always beat it for value. Our exhaustive = tester for bitblt, first done by John Reiser if I remember right, set = the stage for my own thinking about how you properly test something. >=20 > -rob >=20 >=20 > On Thu, May 23, 2024 at 11:49=E2=80=AFPM Douglas McIlroy = > = wrote: >> > Doug McIlroy was generating random regular expressions >>=20 >> Actually not. I exhaustively (within limits) tested an RE recognizer = without knowingly generating any RE either mechanically or by hand. >>=20 >> The trick: =46rom recursive equations (easily derived from the = grammar of REs), I counted how many REs exist up to various limits on = token counts, Then I generated all strings that satisfied those limits, = turned the recognizer loose on them and counted how many it accepted. = Any disagreement of counts revealed the existence (but not any symptom) = of bugs.=20 >>=20 >> Unlike most diagnostic techniques, this scheme produces a certificate = of (very high odds on) correctness over a representative subdomain. The = scheme also agnostically checks behavior on bad inputs as well as good. = It does not, however, provide a stress test of a recognizer's capacity = limits. And its exponential nature limits its applicability to rather = small domains. (REs have only 5 distinct kinds of token.) >>=20 >> Doug --Apple-Mail=_0E6664EE-78A1-4170-9120-208E5206B036 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
What would be nice if programming = languages provided some support for such exhaustive = testing[1].

At one point I had suggested turning = Go's Interface type to something like Guttag style abstract data types = in that relevant axioms are specified right in the interface definition. = The idea was that any concrete type that implements that interface must = satisfy its axioms. Even if the compiler ignored these axioms, one can = write a support program that can generate a set of comprehensive tests = based on these axioms. [Right now a type "implementing" an interface = only needs to have a set of methods that exactly match the interface = methods but nothing more] The underlying idea is that each type is in = essence a constraint on what values an instance of that type can take. = So adding such axioms simply tightens (& documents) these = constraints. Just the process of coming up with such axioms can improve = the design (sor of like test driven design but = better!).

Now it may be that applying this to = anything more complex than stacks won't work well & it won't be = perfect but I thought this was worth experimenting with. This would be = like functional testing of all the nuts and bolts and components that go = in an airplane. The airplane may still fall apart but that would be a = "composition" error!

[1] There are "proof = assisant" or formal spec languages such as TLA+, Coq, Isabelle etc. but = they don't get used much by the average programmer. I want something = more retail!

On May = 23, 2024, at 1:52=E2=80=AFPM, Rob Pike <robpike@gmail.com> = wrote:

The semantic distinction is = important but the end result is very similar. "Fuzzing" as it is now = called (for no reason I can intuit) tries to get to the troublesome = cases faster by a sort of depth-first search, but exhaustive will always = beat it for value. Our exhaustive tester for bitblt, first done by John = Reiser if I remember right, set the stage for my own thinking about how = you properly test something.

-rob


On Thu, May = 23, 2024 at 11:49=E2=80=AFPM Douglas McIlroy <douglas.mcilroy@dartmouth.ed= u> wrote:
> Doug = McIlroy was generating random regular expressions

Actually not. I exhaustively (within limits) = tested an RE recognizer without knowingly generating any RE either = mechanically or by hand.

The = trick: =46rom recursive equations (easily derived from the grammar of = REs), I counted how many REs exist up to various limits on token counts, = Then I generated all strings that satisfied those limits, turned the = recognizer loose on them and counted how many it accepted. Any = disagreement of counts revealed the existence (but not any symptom) of = bugs. 

Unlike most diagnostic techniques, this scheme produces a = certificate of (very high odds on) correctness over a representative = subdomain. The = scheme also agnostically checks behavior on bad inputs as well as = good.  It = does not, however, provide a stress test of a recognizer's capacity = limits. And its = exponential nature limits its applicability to rather small domains. = (REs have only 5 distinct kinds of token.)

Doug

= --Apple-Mail=_0E6664EE-78A1-4170-9120-208E5206B036--