DEV Community: has12zen

Using Cron keep your eyes in check

has12zen — Sun, 26 Sep 2021 16:42:57 +0000

basic syntax for cron

a typical cron job looks like this

# m h  dom mon dow   command
  * *   *   *   *   /usr/bin/sh ls

stand for wildcard this is not a cron tutorial this is just how i use it.

eyes.sh script

the bash script looks like

#!/bin/sh
export DISPLAY=:0
notify-send "EYES CHECK" "Look away for 15 seconds"

without line no 2 it wont work as it sets the display for notify-send. I am using notify-send as my notification daemon.

make sure that your display is :0
you can do this with

echo $DISPLAY

setting up crontab

first you will need to make sure cron is running you can do this by:

systemctl status cronie

p.s. this is specific to arch based system.

once cron is running you can create/edit cron job with crontab -e

then paste the code present below into the window.

*/15 * * * * /usr/bin/sh  /home/elnovo/.noti/eyes.sh

it runs every 15 min and eyes.sh is the bash script we discussed above. save it.
you can find the cron jobs currently present by crontab -l

sources

notify-send doesn't work from crontab

Automatic Program Verification using Dafny

has12zen — Fri, 16 Apr 2021 14:13:41 +0000

Program Verification

Program Verification is the process of proving that the program does exactly what the developer intended it to do and noting more.

basically it can help prevent us from creating something like

not exactly but close enough.

Why testing is not enough

“Testing shows the presence, not the absence of bugs”

-Edsgar W. Dijkstra

For this post HAL is not a super smart AI but a simple program that performs arithmetic operations.
if we were to test HAL he is smart enough to give us correct output for our questions

Hal what is 2 + 2?
HAL: 4
HAL what is 2*2 ?
HAL: 4

HAL gives correct answers to our questions in our test does this mean HAL works as we intended it to work.

Spoiler alert
No

HAL can be returning 2 every time we run it and we wound not notice it with such test. In real life no one will use such small test for their program but even with exhaustive testing we cannot say with 100% confidence that program will work.

So what is the solution?

Formal Methods

Formal methods is just a fancy way of using mathematics in the verification of your program.

Formal methods are really difficult to do and this article is not exactly about them so I'll get straight to the point. but remember that a program that does formal verification for us will take the code we write and what the code is supposed to do from us in order to verify it.

Dafny

Dafny is programming language that helps us in doing formal verification

dafny is close to C# so a lot of thing are similar in dafny.

The most cool thing about Dafny is it can show we are making a mistake while we are writing the code.

Eg:

method Double(x: int) returns (r: int)
   requires  x > 0
   ensures r==2*x
{
   r := x + x;
}

the above code has a method Double which returns the double value of the int it takes in.
The keywords ensures and requires give us a way to specify what the code is supposed to do.
If we make some silly mistake and instead of + we write - dafny will show the error to us

Dafny has a really good guide for learning all of this stuff which you can check out Best Guide and below I will be summarizing what I learned from it.

Summary from what I learnt

Advantages

Can detect bugs while writing code.
Similar to C# and can be installed with VS code extension
Provides a great learning opportunity.

Disadvantages

Dafny uses the Boogie Intermediate language and Z3 SMT solver so is limited by what they both can do.
Dafny cannot be used for existing code we need to write new code to use dafny.

Different parts of Dafny

Method

A method is function which takes zero or more arguments and returns zero or more values. it is differnt than functions present inside dafny. The main method in dafny is Main()
it is not necessary for verification but we need it for getting a .net executable from our code as the execution of code will begins here.

 method Main()
 {

   print "Hello World";
   print "\n";
 }

Function

the keyword function is used for pure functions in dafny. they cannot change the state of program and are ghost by default menas they do not appear in the compiled code. They are used to define mathematical logic.
eg:

function fib(n: nat): nat
{
    if n < 2 then  n
    else
        fib(n - 1) + fib(n - 2)
}

Pre and Post Conditions

They help in specifying the specifications of the program a precondition must be true before the execution of method and a post condition must be true after the execution of the program.

loop invariants

They specify the range of loop condition suppose for a loop i goes from 0 to n then we can specify loop invariants as

while i<n
   invariant 1 <= i <=n
   {
      i := i + 1;
   }
   assert i == n;

They help in dafny in understanding how many times the loop occurs.

Termination

Dafny can automatically determine if a loop will terminate or not

while i<n
       invariant 1 <= i <=n
   {
      i := i + 1; 
       if i<n  {i:= 1;}
       if i==1 {break;}
   }

When we run this code we see dafny knows the code terminates.

Fiboncacci verification using dafny

function fib(n: nat): nat
decreases n
{
    if n < 2 then  n
    else
        fib(n - 1) + fib(n - 2)
}


method ComputeFib(n: nat) returns (b: nat)
    ensures b == fib(n)  
{
    if n == 0 { return 0; }
    var i: int := 1;
    var c := 1;
        b := 1 ;
    while i < n
        invariant  0< i <= n
        invariant b == fib(i)
        invariant c == fib(i + 1)
    {
        b, c := c, b + c;
        i := i + 1;
    }
}


 method Main()
 {
   var result:int := ComputeFib(6);
   print "fib(6):= ";
   print result;
   print "\n";
 }

KWoC Project Report

has12zen — Fri, 08 Jan 2021 09:19:44 +0000

About KWoC

KWOC — Kharagpur Winter of Code is a 5-week long online program organized by KOSS for the students of various colleges, especially for students of IIT Kharagpur, who are new to open source software development.

The Projects I contributed to

During KWoC I contributed to two projects web-development-Resource, url-shortener.

web-development-Resource

Under the direction of my Mentor, I started working on resources of Node.Js, and HTML. In this project, I collected resources and organized them in a structure.

url-shortener

I worked on making the basic structure of the URL-shortener Chrome extension this extension uses Rebrandly API to shorten URLs and also gives QR code for scanning the current URL.

My experience with KWoC

I had quite a good time working on projects in KWoC I always wanted to work on Open source and KWoC finally gave me the push that I needed to get started. I also learned how to effectively communicate with mentors and peers during working on these projects.

Links to the Repos I contributed to

Closed PR's

Used Rebrandly API to shorten link and updated UI #14

has12zen posted on Dec 11, 2020

Pull request template for the-browser-toolbox/url-shortener.

Create a pull request to add your new features or bug fixes.

Description

Used rebrandly API to shorten the URL and also added Qr code panel to display the current page as Qr code

Related Issue

Please link to the related issue here.

Proposed Changes:

using Rebradly API
Adding Qr code panel

Screenshots

Updated Screenshot

Please use the Gitter channel to update about your pull request.

View on GitHub

Added Node.js Resources #14

has12zen posted on Dec 06, 2020

View on GitHub

added HTML resources #17

has12zen posted on Dec 06, 2020

View on GitHub

Open ID protocol

has12zen — Sun, 15 Nov 2020 11:15:47 +0000

Authentication is a very important part of any project. The open id is an open standard and decentralized protocol. It allows users to be authenticated by cooperating sites using third party service, eliminating the need for webmasters to provide their own ad hoc login. Open Id is about authentication (ie. providing who you are).

This protocol provides a way for a site to redirect a user somewhere else and come back with a verifiable assertion. OpenID provides an identity assertion.
The most important feature of OpenID is its discovery process. OpenID does not require hard coding each the providers you want to use ahead of time. Using discovery, the user can choose any third-party provider they want to authenticate. This discovery feature has also caused most of OpenID's problems because the way it is implemented is by using HTTP URIs as identifiers which most web users just don't get.

The scenario for use of OpenID:
1) The user wants to access his account on example.com
2) example.com asks the user for his OpenID
3) The user enters his OpenID
4) example.com redirects the user to his OpenID provider
5) User authenticates himself to the OpenID provider
6) OpenID provider redirects the user back to example.com
7) example.com allows the user to access his account.
search for OAuth or OpenID connect which will help you to know more.