Write a fizzbuzz and then write a formal proof of it's functionality

Write a fizzbuzz and then write a formal proof of it's functionality.

Other urls found in this thread:

lispworks.com/documentation/lw50/CLHS/Body/22_c.htm
twitter.com/SFWRedditGifs

Bumping purely for MOAR

tiny head fat body

Fizzbuzz as mentioned in the original article is for 0 to 100 so the printf is enough to formally prove it

for i in $input
if i % 3 = 0
echo fizz
elsif i % 5 = 0
echo buzz
elseif i % 13 = 0
echo fizzbuzz
end
end

You forgot
else echo i

Write a formal description of fizzbuzz or I am spreading a word about your incompetence.

>elseif

you fucking fail, (unironically)

you can't use else if in fizz buzz dummy

>i % 13

wut

class FizzBuzzCommandlet extends Commandlet;

event int Main(string Parms)
{
local int i;
local string S;

while(i++ < 100)
{
S = "";
if(i % 3 == 0)
S $= "Fizz";
if(i % 5 == 0)
S $= "Buzz";
Log(Eval(S=="",i,S));
}
return 0;
}


>formal proof of its functionality
>mfw running the code is not enough to prove it works

>>mfw running the code is not enough to prove it works
Formally it's not. lrn2math, retard

it's called modulo look it up

modulo?

>mfw running the code is not enough to prove it works
This is why mathematics is important for comp sci majors.
You fucking codemonkey.

serious question, can there be a formal proof of fizzbuzz

Why? I've passed interviews with similar code.

that code doesn't work properly

>13
>elseif

what the fuck? it doesn't work dipshit

you need multiple if statements, not if else

how the fuck are you going to do shit on 15???????/
15 is divisble by 3 AND 5 faggot
but with an if else it's going to say "yes" to 3 and then exit the fucking program

who is

>she

It works if you start with 15 instead of 3 or 5.
There's several other problems though.

yea but you might as well just do if modulu 3 echo and if modulu 5 separate
I saw his 13 too

a fat cow

i%15==0?printf("FizzBuzz\n"):i%5==0?printf("Buzz\n"):i%3==0?printf("Fizz\n"):printf("%d\n", i);

Haskellfags will have a field day with this.

no haskell fags here, they don't exist anymore, as haskell is obsolete
plus, I doubt a haskell fag can into formal proof

>plus, I doubt a haskell fag can into formal proof
Not sure if trolling... When you write code in Haskell, half of the formal proof is already done.

nobody here uses haskell, stop talking nonsense

It's just bait guys OP is sitting in his interview right now and can't answer. Don't help him.

#.(loop for i from 1 to 100 do
(format t "~:[~:[~a~;Buzz~]~;Fizz~:[~;Buzz~]~]~%~@*" (zerop (mod i 3)) (zerop (mod i 5)) i))

where do you learn format strings?

lispworks.com/documentation/lw50/CLHS/Body/22_c.htm

say"Fizz"x!($_%3)."Buzz"x!($_%5)||$_ for 1..100

Why couldn't there be? Draw a circuit and it'll become pretty apparent that it works. I mean you could prove that there are integers that divide by 15, 5, and 3 evenly and some that don't (eg. Something that divides by 2, the lowest prime)

give me an example proof, pls

Read the first chapter of any lambda calculus book, pal.

I've never done a formal proof before, only informal

>says it can be done
>hasn't done one

>I doubt a haskell fag can into formal proof
lowest quality b8 in this thread

Well you're right, turns out I'm retarded. But assuming that I put in 15, and did it first, then wouldn't it work fine? And why is everyone sperging about the elsif?

I'm too brainlet to work out how to represent the truths of prime factorization in conjunction with modulo arithmetic in my head, sorry!

no it wouldn't
why don't you try to fucking run your program and find out what it does?

Surely you don't need to.
Wouldn't the % operator be verified in the spec of the language and then you'd just have to show that your code structure does what you want it to.

Fizz Buzz

holy shit

Looks like a good beat. Post soundcould.

fizzBuzz();

????

that's unreal engine

Rate plez
#!/bin/bash

F="Fizz"
B="Buzz"

fb () {
t=${F[$(($i % 3))]}
f=${B[$(($i % 5))]}
if [ -n "$t" -o -n "$f" ]; then
echo $t$f
else
return 1
fi
}

for i in `seq 1 100`; do
fb || echo $i
done

You can use else if, but only if the first condition tests for i % 15. The remaining cases therefore test for divisibility by 3 and 5 respectfully.

lmao what the fuck is this

Honestly, I don't know why I wasted my time with people who can't even figure out how to install arch linux.

def fizzbuzz(i):
return 'FizzBuzz' if i%5==0 and i%3==0 else ('Fizz' if i%3==0 else ('Buzz' if i%5==0 else i))

:)

Get back in /cum/ schmuck

>still no one has shown a proof for their fizzbuzz

but they proved that it worked

Does anyone here know coq? Sounds very interresding.

Tell me about it?

It's a formal verification framework for programs, I don't know much about it. There's a wikipedia page.

/sci/ here, coq, agda, idris, etc.. are a special class of programming languages called theorem provers. They use dependent types (basically Haskell on steroids) and by abusing the compiler's type checker one is able to verify correctness of theorems (if your CS degree was worth anything this is the part where you recall that theorems = programs).

That said, I don't think you need dependent types to verify correctness of ordinary fizzbuzz. You could probably accomplish the same with Haskell.

lolno

Clever girl

Can somebody coq a fizzbuzz?

I'll cock your fizzbuzz

*I'll cok and fizz in your buzz

>it works
>prove that it works lol
The proof is only relevant if it breaks.

for i in range(1, 101):
fzz = ''
if not i % 3:
fzz += 'fizz'
if not i % 5:
fzz += 'buzz'
print(fzz or i)
The proof writes itself. Also:
>checking 15 or 3 and 5 for divisibility
Fucking plebs, it's sick. If you have more than 2 divisibility checks, you're not a real programmer.

>be told to implement an autopilot system for a plane.
>be told to prove that the implementation is correct.
Kek the proof is only relevant if the plane crashes.

Not only is that wrong but if it breaks it means the proof DOES NOT EXIST.

this is why I use haskell

patrician language coming through

with Ada.Text_IO;
use Ada.Text_IO;

procedure fizzbuzz is
subtype fizz is Integer with Dynamic_Predicate => fizz mod 3 = 0;
subtype buzz is Integer with Dynamic_Predicate => buzz mod 5 = 0;
begin
for i in 1..100 loop
put(i'Img & " ");
if(i in fizz) then
put("Fizz");
end if;
if(i in buzz) then
put("Buzz");
end if;
New_Line;
end loop;
end fizzbuzz;


when will hiroshima add Ada highlighting to Sup Forums

You tried so hard and got so far. But in the end, it doesn't even matter.

What colouring does Sup Forums use?

if some number is divisible by 3 : fizz
else if that number is divisible by 5 : buzz
else if both divisible by 3 and 5 : fizz buzz
otherwise : do nothing and increment that number

package main

import "fmt"

func getFizzBuzzText(number int) string {
if number%3 == 0 && number%5 == 0 {
return "FizzBuzz"
}
if number%3 == 0 {
return "Fizz"
}
if number%5 == 0 {
return "Buzz"
}
return fmt.Sprintf("%d", number)
}

func fizzBuzzService(in

otherwise : print number

for x in range(1,101):print(x%3==0)*"Fizz"+(x%5==0)*"Buzz"or x


\documentclass{article}
\usepackage{amsmath}
\begin{document}

\title{Formal FizzBuzz Proof}
\author{Landon J. Powell}
\maketitle

$$
A = [1, 2, "Fizz", 4, "Buzz", ..., 98, "Fizz", "Buzz"]
$$

$$
f(x) = \left\{
\begin{array}{ll}
"FizzBuzz" & \quad x \bmod 15 = 0 \\
"Fizz" & \quad x \bmod 3 = 0 \\
"Buzz" & \quad x \bmod 5 = 0 \\
x
\end{array}
\right.
$$

$$
B = f(i) \text{ for } i = 1, ..., 100
$$

$$
B = A
$$

\end{document}


I can barely remember my piecewise functions.

That is not a formal proof. Even if it was, that isn't FizzBuzz.

Are those dependent types?

>user can you write us a program.
Sure thing! Let me just create a formal proof of it first.

Except it works retard. Most jobs don't even require proofs just testing to sigma X to show it works suffiently. On another note in a pure math fashion fizzbuzz would fall short with its 2^31-1 limit.

>would fall short with its 2^31-1 limit.
>pure math

>On another note in a pure math fashion fizzbuzz would fall short with its 2^31-1 limit.
You are clearly brain damaged.

1. In pure math one does not care about the physical world and limitations like that do not matter at all.
2. In a proof one would state a precondition that the numbers given must fall within that range. Alternatively one may allow for larger numbers by properly implementing bignum functionality together with a fast bignum modular division. Such an implementation would likely not only call for a proof of correctness but also a proof of runtime efficiency (as the code would need to be more complicated to handle this sort of thing).

Just because your "jobs" don't require proofs doesn't mean that when asked for a proof it is appropriate to say "but my mommy told me I don't need them most of the time".

Tests are literally placebos and test driven development is garbage for brainlet codemonkeys who are barely even allowed behind a keyboard (inb4 b-b-but that means most software developers are brainlet codemonkeys).

You cannot sufficiently argue that it works unless you can prove it.

(1) is reasonable
(2) turbo autism

int main() {

int i;
for (i=0; i

In principle yes
The number i is part of the subtypes if it fits the predicate condition i mod 3 = 0 for example

Isn't a correct code a proof in itself? You just 'constructed' the proof.

SImple

>then write a formal proof

>

Do it faggot.

>You could probably accomplish the same with Haskell.
In Haskell every type is inhabited so I wouldn't trust any """proof """ that comes out of it.

Nope.

>In principle yes
No.

fizzbuzz n | n > 2 = fizzbuzzer [[x] | x

Why didn't I at least use
fizzbuzzer ([x]:xs) ys
instead?

I hope you'll never work on anything related to self driving vehicles, nor traffic management system.

Would they even hire someone of his kind?

What properties of fizzbuzz would one have to prove to consider that a formal proof of fizzbuzz?

You fucking idiot, FizzButt is defined in [0, 100]. printf is sufficient for a proof (exhaustion).